Lemmas about liminf and limsup in an order topology. #
Main declarations #
BoundedLENhdsClass: Typeclass stating that neighborhoods are eventually bounded above.BoundedGENhdsClass: Typeclass stating that neighborhoods are eventually bounded below.
Implementation notes #
The same lemmas are true in ℝ, ℝ × ℝ, ι → ℝ, EuclideanSpace ι ℝ. To avoid code
duplication, we provide an ad hoc axiomatisation of the properties we need.
Ad hoc typeclass stating that neighborhoods are eventually bounded above.
- isBounded_le_nhds : ∀ (a : α), Filter.IsBounded (fun (x1 x2 : α) => x1 ≤ x2) (nhds a)
Instances
Ad hoc typeclass stating that neighborhoods are eventually bounded below.
- isBounded_ge_nhds : ∀ (a : α), Filter.IsBounded (fun (x1 x2 : α) => x1 ≥ x2) (nhds a)
Instances
theorem
isBounded_le_nhds
{α : Type u_2}
[Preorder α]
[TopologicalSpace α]
[BoundedLENhdsClass α]
(a : α)
:
Filter.IsBounded (fun (x1 x2 : α) => x1 ≤ x2) (nhds a)
theorem
Filter.Tendsto.isBoundedUnder_le
{ι : Type u_1}
{α : Type u_2}
[Preorder α]
[TopologicalSpace α]
[BoundedLENhdsClass α]
{f : Filter ι}
{u : ι → α}
{a : α}
(h : Filter.Tendsto u f (nhds a))
:
Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u
theorem
Filter.Tendsto.bddAbove_range_of_cofinite
{ι : Type u_1}
{α : Type u_2}
[Preorder α]
[TopologicalSpace α]
[BoundedLENhdsClass α]
{u : ι → α}
{a : α}
[IsDirected α fun (x1 x2 : α) => x1 ≤ x2]
(h : Filter.Tendsto u Filter.cofinite (nhds a))
:
theorem
Filter.Tendsto.bddAbove_range
{α : Type u_2}
[Preorder α]
[TopologicalSpace α]
[BoundedLENhdsClass α]
{a : α}
[IsDirected α fun (x1 x2 : α) => x1 ≤ x2]
{u : ℕ → α}
(h : Filter.Tendsto u Filter.atTop (nhds a))
:
theorem
isCobounded_ge_nhds
{α : Type u_2}
[Preorder α]
[TopologicalSpace α]
[BoundedLENhdsClass α]
(a : α)
:
Filter.IsCobounded (fun (x1 x2 : α) => x1 ≥ x2) (nhds a)
theorem
Filter.Tendsto.isCoboundedUnder_ge
{ι : Type u_1}
{α : Type u_2}
[Preorder α]
[TopologicalSpace α]
[BoundedLENhdsClass α]
{f : Filter ι}
{u : ι → α}
{a : α}
[f.NeBot]
(h : Filter.Tendsto u f (nhds a))
:
Filter.IsCoboundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u
instance
instBoundedGENhdsClassOrderDual
{α : Type u_2}
[Preorder α]
[TopologicalSpace α]
[BoundedLENhdsClass α]
:
Equations
- ⋯ = ⋯
instance
Prod.instBoundedLENhdsClass
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[TopologicalSpace α]
[TopologicalSpace β]
[BoundedLENhdsClass α]
[BoundedLENhdsClass β]
:
BoundedLENhdsClass (α × β)
Equations
- ⋯ = ⋯
instance
Pi.instBoundedLENhdsClass
{ι : Type u_1}
{π : ι → Type u_6}
[Finite ι]
[(i : ι) → Preorder (π i)]
[(i : ι) → TopologicalSpace (π i)]
[∀ (i : ι), BoundedLENhdsClass (π i)]
:
BoundedLENhdsClass ((i : ι) → π i)
Equations
- ⋯ = ⋯
theorem
isBounded_ge_nhds
{α : Type u_2}
[Preorder α]
[TopologicalSpace α]
[BoundedGENhdsClass α]
(a : α)
:
Filter.IsBounded (fun (x1 x2 : α) => x1 ≥ x2) (nhds a)
theorem
Filter.Tendsto.isBoundedUnder_ge
{ι : Type u_1}
{α : Type u_2}
[Preorder α]
[TopologicalSpace α]
[BoundedGENhdsClass α]
{f : Filter ι}
{u : ι → α}
{a : α}
(h : Filter.Tendsto u f (nhds a))
:
Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u
theorem
Filter.Tendsto.bddBelow_range_of_cofinite
{ι : Type u_1}
{α : Type u_2}
[Preorder α]
[TopologicalSpace α]
[BoundedGENhdsClass α]
{u : ι → α}
{a : α}
[IsDirected α fun (x1 x2 : α) => x1 ≥ x2]
(h : Filter.Tendsto u Filter.cofinite (nhds a))
:
theorem
Filter.Tendsto.bddBelow_range
{α : Type u_2}
[Preorder α]
[TopologicalSpace α]
[BoundedGENhdsClass α]
{a : α}
[IsDirected α fun (x1 x2 : α) => x1 ≥ x2]
{u : ℕ → α}
(h : Filter.Tendsto u Filter.atTop (nhds a))
:
theorem
isCobounded_le_nhds
{α : Type u_2}
[Preorder α]
[TopologicalSpace α]
[BoundedGENhdsClass α]
(a : α)
:
Filter.IsCobounded (fun (x1 x2 : α) => x1 ≤ x2) (nhds a)
theorem
Filter.Tendsto.isCoboundedUnder_le
{ι : Type u_1}
{α : Type u_2}
[Preorder α]
[TopologicalSpace α]
[BoundedGENhdsClass α]
{f : Filter ι}
{u : ι → α}
{a : α}
[f.NeBot]
(h : Filter.Tendsto u f (nhds a))
:
Filter.IsCoboundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u
instance
instBoundedLENhdsClassOrderDual
{α : Type u_2}
[Preorder α]
[TopologicalSpace α]
[BoundedGENhdsClass α]
:
Equations
- ⋯ = ⋯
instance
Prod.instBoundedGENhdsClass
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[TopologicalSpace α]
[TopologicalSpace β]
[BoundedGENhdsClass α]
[BoundedGENhdsClass β]
:
BoundedGENhdsClass (α × β)
Equations
- ⋯ = ⋯
instance
Pi.instBoundedGENhdsClass
{ι : Type u_1}
{π : ι → Type u_6}
[Finite ι]
[(i : ι) → Preorder (π i)]
[(i : ι) → TopologicalSpace (π i)]
[∀ (i : ι), BoundedGENhdsClass (π i)]
:
BoundedGENhdsClass ((i : ι) → π i)
Equations
- ⋯ = ⋯
@[instance 100]
instance
OrderTop.to_BoundedLENhdsClass
{α : Type u_2}
[Preorder α]
[TopologicalSpace α]
[OrderTop α]
:
Equations
- ⋯ = ⋯
@[instance 100]
instance
OrderBot.to_BoundedGENhdsClass
{α : Type u_2}
[Preorder α]
[TopologicalSpace α]
[OrderBot α]
:
Equations
- ⋯ = ⋯
@[instance 100]
instance
BoundedLENhdsClass.of_closedIciTopology
{α : Type u_2}
[LinearOrder α]
[TopologicalSpace α]
[ClosedIciTopology α]
:
Equations
- ⋯ = ⋯
@[instance 100]
instance
BoundedGENhdsClass.of_closedIicTopology
{α : Type u_2}
[LinearOrder α]
[TopologicalSpace α]
[ClosedIicTopology α]
:
Equations
- ⋯ = ⋯
theorem
le_nhds_of_limsSup_eq_limsInf
{α : Type u_2}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
{f : Filter α}
{a : α}
(hl : Filter.IsBounded (fun (x1 x2 : α) => x1 ≤ x2) f)
(hg : Filter.IsBounded (fun (x1 x2 : α) => x1 ≥ x2) f)
(hs : f.limsSup = a)
(hi : f.limsInf = a)
:
If the liminf and the limsup of a filter coincide, then this filter converges to their common value, at least if the filter is eventually bounded above and below.
theorem
limsSup_nhds
{α : Type u_2}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
(a : α)
:
theorem
limsInf_nhds
{α : Type u_2}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
(a : α)
:
theorem
limsInf_eq_of_le_nhds
{α : Type u_2}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
{f : Filter α}
{a : α}
[f.NeBot]
(h : f ≤ nhds a)
:
f.limsInf = a
If a filter is converging, its limsup coincides with its limit.
theorem
limsSup_eq_of_le_nhds
{α : Type u_2}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
{f : Filter α}
{a : α}
[f.NeBot]
(h : f ≤ nhds a)
:
f.limsSup = a
If a filter is converging, its liminf coincides with its limit.
theorem
Filter.Tendsto.limsup_eq
{α : Type u_2}
{β : Type u_3}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
{f : Filter β}
{u : β → α}
{a : α}
[f.NeBot]
(h : Filter.Tendsto u f (nhds a))
:
Filter.limsup u f = a
If a function has a limit, then its limsup coincides with its limit.
theorem
Filter.Tendsto.liminf_eq
{α : Type u_2}
{β : Type u_3}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
{f : Filter β}
{u : β → α}
{a : α}
[f.NeBot]
(h : Filter.Tendsto u f (nhds a))
:
Filter.liminf u f = a
If a function has a limit, then its liminf coincides with its limit.
theorem
tendsto_of_liminf_eq_limsup
{α : Type u_2}
{β : Type u_3}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
{f : Filter β}
{u : β → α}
{a : α}
(hinf : Filter.liminf u f = a)
(hsup : Filter.limsup u f = a)
(h : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u := by isBoundedDefault)
(h' : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u := by isBoundedDefault)
:
Filter.Tendsto u f (nhds a)
If the liminf and the limsup of a function coincide, then the limit of the function exists and has the same value.
theorem
tendsto_of_le_liminf_of_limsup_le
{α : Type u_2}
{β : Type u_3}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
{f : Filter β}
{u : β → α}
{a : α}
(hinf : a ≤ Filter.liminf u f)
(hsup : Filter.limsup u f ≤ a)
(h : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u := by isBoundedDefault)
(h' : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u := by isBoundedDefault)
:
Filter.Tendsto u f (nhds a)
If a number a is less than or equal to the liminf of a function f at some filter
and is greater than or equal to the limsup of f, then f tends to a along this filter.
theorem
tendsto_of_no_upcrossings
{α : Type u_2}
{β : Type u_3}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
[DenselyOrdered α]
{f : Filter β}
{u : β → α}
{s : Set α}
(hs : Dense s)
(H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n))
(h : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u := by isBoundedDefault)
(h' : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u := by isBoundedDefault)
:
∃ (c : α), Filter.Tendsto u f (nhds c)
Assume that, for any a < b, a sequence can not be infinitely many times below a and
above b. If it is also ultimately bounded above and below, then it has to converge. This even
works if a and b are restricted to a dense subset.
theorem
eventually_le_limsup
{α : Type u_2}
{β : Type u_3}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
[FirstCountableTopology α]
{f : Filter β}
[CountableInterFilter f]
{u : β → α}
(hf : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u := by isBoundedDefault)
:
∀ᶠ (b : β) in f, u b ≤ Filter.limsup u f
theorem
eventually_liminf_le
{α : Type u_2}
{β : Type u_3}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
[FirstCountableTopology α]
{f : Filter β}
[CountableInterFilter f]
{u : β → α}
(hf : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u := by isBoundedDefault)
:
∀ᶠ (b : β) in f, Filter.liminf u f ≤ u b
@[simp]
theorem
limsup_eq_bot
{α : Type u_2}
{β : Type u_3}
[CompleteLinearOrder α]
[TopologicalSpace α]
[FirstCountableTopology α]
[OrderTopology α]
{f : Filter β}
[CountableInterFilter f]
{u : β → α}
:
@[simp]
theorem
liminf_eq_top
{α : Type u_2}
{β : Type u_3}
[CompleteLinearOrder α]
[TopologicalSpace α]
[FirstCountableTopology α]
[OrderTopology α]
{f : Filter β}
[CountableInterFilter f]
{u : β → α}
:
theorem
Antitone.map_limsSup_of_continuousAt
{R : Type u_4}
{S : Type u_5}
[ConditionallyCompleteLinearOrder R]
[TopologicalSpace R]
[OrderTopology R]
[ConditionallyCompleteLinearOrder S]
[TopologicalSpace S]
[OrderTopology S]
{F : Filter R}
[F.NeBot]
{f : R → S}
(f_decr : Antitone f)
(f_cont : ContinuousAt f F.limsSup)
(bdd_above : Filter.IsBounded (fun (x1 x2 : R) => x1 ≤ x2) F := by isBoundedDefault)
(cobdd : Filter.IsCobounded (fun (x1 x2 : R) => x1 ≤ x2) F := by isBoundedDefault)
:
f F.limsSup = Filter.liminf f F
An antitone function between (conditionally) complete linear ordered spaces sends a
Filter.limsSup to the Filter.liminf of the image if the function is continuous at the limsSup
(and the filter is bounded from above and frequently bounded from below).
theorem
Antitone.map_limsup_of_continuousAt
{ι : Type u_1}
{R : Type u_4}
{S : Type u_5}
{F : Filter ι}
[F.NeBot]
[ConditionallyCompleteLinearOrder R]
[TopologicalSpace R]
[OrderTopology R]
[ConditionallyCompleteLinearOrder S]
[TopologicalSpace S]
[OrderTopology S]
{f : R → S}
(f_decr : Antitone f)
(a : ι → R)
(f_cont : ContinuousAt f (Filter.limsup a F))
(bdd_above : Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 ≤ x2) F a := by isBoundedDefault)
(cobdd : Filter.IsCoboundedUnder (fun (x1 x2 : R) => x1 ≤ x2) F a := by isBoundedDefault)
:
f (Filter.limsup a F) = Filter.liminf (f ∘ a) F
A continuous antitone function between (conditionally) complete linear ordered spaces sends a
Filter.limsup to the Filter.liminf of the images (if the filter is bounded from above and
frequently bounded from below).
theorem
Antitone.map_limsInf_of_continuousAt
{R : Type u_4}
{S : Type u_5}
[ConditionallyCompleteLinearOrder R]
[TopologicalSpace R]
[OrderTopology R]
[ConditionallyCompleteLinearOrder S]
[TopologicalSpace S]
[OrderTopology S]
{F : Filter R}
[F.NeBot]
{f : R → S}
(f_decr : Antitone f)
(f_cont : ContinuousAt f F.limsInf)
(cobdd : Filter.IsCobounded (fun (x1 x2 : R) => x1 ≥ x2) F := by isBoundedDefault)
(bdd_below : Filter.IsBounded (fun (x1 x2 : R) => x1 ≥ x2) F := by isBoundedDefault)
:
f F.limsInf = Filter.limsup f F
An antitone function between (conditionally) complete linear ordered spaces sends a
Filter.limsInf to the Filter.limsup of the image if the function is continuous at the limsInf
(and the filter is bounded from below and frequently bounded from above).
theorem
Antitone.map_liminf_of_continuousAt
{ι : Type u_1}
{R : Type u_4}
{S : Type u_5}
{F : Filter ι}
[F.NeBot]
[ConditionallyCompleteLinearOrder R]
[TopologicalSpace R]
[OrderTopology R]
[ConditionallyCompleteLinearOrder S]
[TopologicalSpace S]
[OrderTopology S]
{f : R → S}
(f_decr : Antitone f)
(a : ι → R)
(f_cont : ContinuousAt f (Filter.liminf a F))
(cobdd : Filter.IsCoboundedUnder (fun (x1 x2 : R) => x1 ≥ x2) F a := by isBoundedDefault)
(bdd_below : Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 ≥ x2) F a := by isBoundedDefault)
:
f (Filter.liminf a F) = Filter.limsup (f ∘ a) F
A continuous antitone function between (conditionally) complete linear ordered spaces sends a
Filter.liminf to the Filter.limsup of the images (if the filter is bounded from below and
frequently bounded from above).
theorem
Monotone.map_limsSup_of_continuousAt
{R : Type u_4}
{S : Type u_5}
[ConditionallyCompleteLinearOrder R]
[TopologicalSpace R]
[OrderTopology R]
[ConditionallyCompleteLinearOrder S]
[TopologicalSpace S]
[OrderTopology S]
{F : Filter R}
[F.NeBot]
{f : R → S}
(f_incr : Monotone f)
(f_cont : ContinuousAt f F.limsSup)
(bdd_above : Filter.IsBounded (fun (x1 x2 : R) => x1 ≤ x2) F := by isBoundedDefault)
(cobdd : Filter.IsCobounded (fun (x1 x2 : R) => x1 ≤ x2) F := by isBoundedDefault)
:
f F.limsSup = Filter.limsup f F
A monotone function between (conditionally) complete linear ordered spaces sends a
Filter.limsSup to the Filter.limsup of the image if the function is continuous at the limsSup
(and the filter is bounded from above and frequently bounded from below).
theorem
Monotone.map_limsup_of_continuousAt
{ι : Type u_1}
{R : Type u_4}
{S : Type u_5}
{F : Filter ι}
[F.NeBot]
[ConditionallyCompleteLinearOrder R]
[TopologicalSpace R]
[OrderTopology R]
[ConditionallyCompleteLinearOrder S]
[TopologicalSpace S]
[OrderTopology S]
{f : R → S}
(f_incr : Monotone f)
(a : ι → R)
(f_cont : ContinuousAt f (Filter.limsup a F))
(bdd_above : Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 ≤ x2) F a := by isBoundedDefault)
(cobdd : Filter.IsCoboundedUnder (fun (x1 x2 : R) => x1 ≤ x2) F a := by isBoundedDefault)
:
f (Filter.limsup a F) = Filter.limsup (f ∘ a) F
A continuous monotone function between (conditionally) complete linear ordered spaces sends a
Filter.limsup to the Filter.limsup of the images (if the filter is bounded from above and
frequently bounded from below).
theorem
Monotone.map_limsInf_of_continuousAt
{R : Type u_4}
{S : Type u_5}
[ConditionallyCompleteLinearOrder R]
[TopologicalSpace R]
[OrderTopology R]
[ConditionallyCompleteLinearOrder S]
[TopologicalSpace S]
[OrderTopology S]
{F : Filter R}
[F.NeBot]
{f : R → S}
(f_incr : Monotone f)
(f_cont : ContinuousAt f F.limsInf)
(cobdd : Filter.IsCobounded (fun (x1 x2 : R) => x1 ≥ x2) F := by isBoundedDefault)
(bdd_below : Filter.IsBounded (fun (x1 x2 : R) => x1 ≥ x2) F := by isBoundedDefault)
:
f F.limsInf = Filter.liminf f F
A monotone function between (conditionally) complete linear ordered spaces sends a
Filter.limsInf to the Filter.liminf of the image if the function is continuous at the limsInf
(and the filter is bounded from below and frequently bounded from above).
theorem
Monotone.map_liminf_of_continuousAt
{ι : Type u_1}
{R : Type u_4}
{S : Type u_5}
{F : Filter ι}
[F.NeBot]
[ConditionallyCompleteLinearOrder R]
[TopologicalSpace R]
[OrderTopology R]
[ConditionallyCompleteLinearOrder S]
[TopologicalSpace S]
[OrderTopology S]
{f : R → S}
(f_incr : Monotone f)
(a : ι → R)
(f_cont : ContinuousAt f (Filter.liminf a F))
(cobdd : Filter.IsCoboundedUnder (fun (x1 x2 : R) => x1 ≥ x2) F a := by isBoundedDefault)
(bdd_below : Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 ≥ x2) F a := by isBoundedDefault)
:
f (Filter.liminf a F) = Filter.liminf (f ∘ a) F
A continuous monotone function between (conditionally) complete linear ordered spaces sends a
Filter.liminf to the Filter.liminf of the images (if the filter is bounded from below and
frequently bounded from above).
theorem
limsup_eq_tendsto_sum_indicator_nat_atTop
{α : Type u_2}
(s : ℕ → Set α)
:
Filter.limsup s Filter.atTop = {ω : α | Filter.Tendsto (fun (n : ℕ) => ∑ k ∈ Finset.range n, (s (k + 1)).indicator 1 ω) Filter.atTop Filter.atTop}
theorem
limsup_eq_tendsto_sum_indicator_atTop
{α : Type u_2}
(R : Type u_7)
[StrictOrderedSemiring R]
[Archimedean R]
(s : ℕ → Set α)
:
Filter.limsup s Filter.atTop = {ω : α | Filter.Tendsto (fun (n : ℕ) => ∑ k ∈ Finset.range n, (s (k + 1)).indicator 1 ω) Filter.atTop Filter.atTop}
theorem
le_limsup_add
{ι : Type u_1}
{α : Type u_2}
[AddCommGroup α]
[ConditionallyCompleteLinearOrder α]
[DenselyOrdered α]
[CovariantClass α α (fun (a b : α) => a + b) fun (x1 x2 : α) => x1 ≤ x2]
{f : Filter ι}
[f.NeBot]
{u v : ι → α}
(h₁ : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u := by isBoundedDefault)
(h₂ : Filter.IsCoboundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u := by isBoundedDefault)
(h₃ : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f v := by isBoundedDefault)
(h₄ : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f v := by isBoundedDefault)
:
Filter.limsup u f + Filter.liminf v f ≤ Filter.limsup (u + v) f
theorem
limsup_add_le
{ι : Type u_1}
{α : Type u_2}
[AddCommGroup α]
[ConditionallyCompleteLinearOrder α]
[DenselyOrdered α]
[CovariantClass α α (fun (a b : α) => a + b) fun (x1 x2 : α) => x1 ≤ x2]
{f : Filter ι}
[f.NeBot]
{u v : ι → α}
(h₁ : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u := by isBoundedDefault)
(h₂ : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u := by isBoundedDefault)
(h₃ : Filter.IsCoboundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f v := by isBoundedDefault)
(h₄ : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f v := by isBoundedDefault)
:
Filter.limsup (u + v) f ≤ Filter.limsup u f + Filter.limsup v f
theorem
le_liminf_add
{ι : Type u_1}
{α : Type u_2}
[AddCommGroup α]
[ConditionallyCompleteLinearOrder α]
[DenselyOrdered α]
[CovariantClass α α (fun (a b : α) => a + b) fun (x1 x2 : α) => x1 ≤ x2]
{f : Filter ι}
[f.NeBot]
{u v : ι → α}
(h₁ : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u := by isBoundedDefault)
(h₂ : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u := by isBoundedDefault)
(h₃ : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f v := by isBoundedDefault)
(h₄ : Filter.IsCoboundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f v := by isBoundedDefault)
:
Filter.liminf u f + Filter.liminf v f ≤ Filter.liminf (u + v) f
theorem
liminf_add_le
{ι : Type u_1}
{α : Type u_2}
[AddCommGroup α]
[ConditionallyCompleteLinearOrder α]
[DenselyOrdered α]
[CovariantClass α α (fun (a b : α) => a + b) fun (x1 x2 : α) => x1 ≤ x2]
{f : Filter ι}
[f.NeBot]
{u v : ι → α}
(h₁ : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u := by isBoundedDefault)
(h₂ : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u := by isBoundedDefault)
(h₃ : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f v := by isBoundedDefault)
(h₄ : Filter.IsCoboundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f v := by isBoundedDefault)
:
Filter.liminf (u + v) f ≤ Filter.limsup u f + Filter.liminf v f
theorem
le_limsup_mul
{ι : Type u_1}
{f : Filter ι}
[f.NeBot]
{u v : ι → ℝ}
(h₁ : 0 ≤ᶠ[f] u)
(h₂ : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) f u)
(h₃ : 0 ≤ᶠ[f] v)
(h₄ : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) f v)
:
Filter.limsup u f * Filter.liminf v f ≤ Filter.limsup (u * v) f
theorem
limsup_mul_le
{ι : Type u_1}
{f : Filter ι}
[f.NeBot]
{u v : ι → ℝ}
(h₁ : 0 ≤ᶠ[f] u)
(h₂ : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) f u)
(h₃ : 0 ≤ᶠ[f] v)
(h₄ : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) f v)
:
Filter.limsup (u * v) f ≤ Filter.limsup u f * Filter.limsup v f
theorem
le_liminf_mul
{ι : Type u_1}
{f : Filter ι}
[f.NeBot]
{u v : ι → ℝ}
(h₁ : 0 ≤ᶠ[f] u)
(h₂ : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) f u)
(h₃ : 0 ≤ᶠ[f] v)
(h₄ : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) f v)
:
Filter.liminf u f * Filter.liminf v f ≤ Filter.liminf (u * v) f
theorem
liminf_mul_le
{ι : Type u_1}
{f : Filter ι}
[f.NeBot]
{u v : ι → ℝ}
(h₁ : 0 ≤ᶠ[f] u)
(h₂ : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) f u)
(h₃ : 0 ≤ᶠ[f] v)
(h₄ : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) f v)
:
Filter.liminf (u * v) f ≤ Filter.limsup u f * Filter.liminf v f
theorem
limsup_const_add
{ι : Type u_1}
{R : Type u_4}
[ConditionallyCompleteLinearOrder R]
[TopologicalSpace R]
[OrderTopology R]
(F : Filter ι)
[F.NeBot]
[Add R]
[ContinuousAdd R]
[AddLeftMono R]
(f : ι → R)
(c : R)
(bdd_above : Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 ≤ x2) F f)
(cobdd : Filter.IsCoboundedUnder (fun (x1 x2 : R) => x1 ≤ x2) F f)
:
Filter.limsup (fun (i : ι) => c + f i) F = c + Filter.limsup f F
liminf (c + xᵢ) = c + liminf xᵢ.
theorem
limsup_add_const
{ι : Type u_1}
{R : Type u_4}
[ConditionallyCompleteLinearOrder R]
[TopologicalSpace R]
[OrderTopology R]
(F : Filter ι)
[F.NeBot]
[Add R]
[ContinuousAdd R]
[AddRightMono R]
(f : ι → R)
(c : R)
(bdd_above : Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 ≤ x2) F f)
(cobdd : Filter.IsCoboundedUnder (fun (x1 x2 : R) => x1 ≤ x2) F f)
:
Filter.limsup (fun (i : ι) => f i + c) F = Filter.limsup f F + c
limsup (xᵢ + c) = (limsup xᵢ) + c.
theorem
liminf_const_add
{ι : Type u_1}
{R : Type u_4}
[ConditionallyCompleteLinearOrder R]
[TopologicalSpace R]
[OrderTopology R]
(F : Filter ι)
[F.NeBot]
[Add R]
[ContinuousAdd R]
[AddLeftMono R]
(f : ι → R)
(c : R)
(cobdd : Filter.IsCoboundedUnder (fun (x1 x2 : R) => x1 ≥ x2) F f)
(bdd_below : Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 ≥ x2) F f)
:
Filter.liminf (fun (i : ι) => c + f i) F = c + Filter.liminf f F
liminf (c + xᵢ) = c + limsup xᵢ.
theorem
liminf_add_const
{ι : Type u_1}
{R : Type u_4}
[ConditionallyCompleteLinearOrder R]
[TopologicalSpace R]
[OrderTopology R]
(F : Filter ι)
[F.NeBot]
[Add R]
[ContinuousAdd R]
[AddRightMono R]
(f : ι → R)
(c : R)
(cobdd : Filter.IsCoboundedUnder (fun (x1 x2 : R) => x1 ≥ x2) F f)
(bdd_below : Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 ≥ x2) F f)
:
Filter.liminf (fun (i : ι) => f i + c) F = Filter.liminf f F + c
liminf (xᵢ + c) = (liminf xᵢ) + c.
theorem
limsup_const_sub
{ι : Type u_1}
{R : Type u_4}
[ConditionallyCompleteLinearOrder R]
[TopologicalSpace R]
[OrderTopology R]
(F : Filter ι)
[AddCommSemigroup R]
[Sub R]
[ContinuousSub R]
[OrderedSub R]
[AddLeftMono R]
(f : ι → R)
(c : R)
(cobdd : Filter.IsCoboundedUnder (fun (x1 x2 : R) => x1 ≥ x2) F f)
(bdd_below : Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 ≥ x2) F f)
:
Filter.limsup (fun (i : ι) => c - f i) F = c - Filter.liminf f F
limsup (c - xᵢ) = c - liminf xᵢ.
theorem
limsup_sub_const
{ι : Type u_1}
{R : Type u_4}
[ConditionallyCompleteLinearOrder R]
[TopologicalSpace R]
[OrderTopology R]
(F : Filter ι)
[AddCommSemigroup R]
[Sub R]
[ContinuousSub R]
[OrderedSub R]
(f : ι → R)
(c : R)
(bdd_above : Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 ≤ x2) F f)
(cobdd : Filter.IsCoboundedUnder (fun (x1 x2 : R) => x1 ≤ x2) F f)
:
Filter.limsup (fun (i : ι) => f i - c) F = Filter.limsup f F - c
limsup (xᵢ - c) = (limsup xᵢ) - c.
theorem
liminf_const_sub
{ι : Type u_1}
{R : Type u_4}
[ConditionallyCompleteLinearOrder R]
[TopologicalSpace R]
[OrderTopology R]
(F : Filter ι)
[F.NeBot]
[AddCommSemigroup R]
[Sub R]
[ContinuousSub R]
[OrderedSub R]
[AddLeftMono R]
(f : ι → R)
(c : R)
(bdd_above : Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 ≤ x2) F f)
(cobdd : Filter.IsCoboundedUnder (fun (x1 x2 : R) => x1 ≤ x2) F f)
:
Filter.liminf (fun (i : ι) => c - f i) F = c - Filter.limsup f F
liminf (c - xᵢ) = c - limsup xᵢ.
theorem
liminf_sub_const
{ι : Type u_1}
{R : Type u_4}
[ConditionallyCompleteLinearOrder R]
[TopologicalSpace R]
[OrderTopology R]
(F : Filter ι)
[F.NeBot]
[AddCommSemigroup R]
[Sub R]
[ContinuousSub R]
[OrderedSub R]
(f : ι → R)
(c : R)
(cobdd : Filter.IsCoboundedUnder (fun (x1 x2 : R) => x1 ≥ x2) F f)
(bdd_below : Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 ≥ x2) F f)
:
Filter.liminf (fun (i : ι) => f i - c) F = Filter.liminf f F - c
liminf (xᵢ - c) = (liminf xᵢ) - c.