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 : Tendsto u f (nhds a))
:
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 : Tendsto u cofinite (nhds a))
:
theorem
Filter.Tendsto.bddAbove_range
{α : Type u_2}
[Preorder α]
[TopologicalSpace α]
[BoundedLENhdsClass α]
{a : α}
[IsDirected α fun (x1 x2 : α) => x1 ≤ x2]
{u : ℕ → α}
(h : Tendsto u 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 : Tendsto u f (nhds a))
:
IsCoboundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u
instance
instBoundedGENhdsClassOrderDual
{α : Type u_2}
[Preorder α]
[TopologicalSpace α]
[BoundedLENhdsClass α]
:
instance
Prod.instBoundedLENhdsClass
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[TopologicalSpace α]
[TopologicalSpace β]
[BoundedLENhdsClass α]
[BoundedLENhdsClass β]
:
BoundedLENhdsClass (α × β)
instance
Pi.instBoundedLENhdsClass
{ι : Type u_1}
{π : ι → Type u_6}
[Finite ι]
[(i : ι) → Preorder (π i)]
[(i : ι) → TopologicalSpace (π i)]
[∀ (i : ι), BoundedLENhdsClass (π i)]
:
BoundedLENhdsClass ((i : ι) → π i)
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 : Tendsto u f (nhds a))
:
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 : Tendsto u cofinite (nhds a))
:
theorem
Filter.Tendsto.bddBelow_range
{α : Type u_2}
[Preorder α]
[TopologicalSpace α]
[BoundedGENhdsClass α]
{a : α}
[IsDirected α fun (x1 x2 : α) => x1 ≥ x2]
{u : ℕ → α}
(h : Tendsto u 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 : Tendsto u f (nhds a))
:
IsCoboundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u
instance
instBoundedLENhdsClassOrderDual
{α : Type u_2}
[Preorder α]
[TopologicalSpace α]
[BoundedGENhdsClass α]
:
instance
Prod.instBoundedGENhdsClass
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[Preorder β]
[TopologicalSpace α]
[TopologicalSpace β]
[BoundedGENhdsClass α]
[BoundedGENhdsClass β]
:
BoundedGENhdsClass (α × β)
instance
Pi.instBoundedGENhdsClass
{ι : Type u_1}
{π : ι → Type u_6}
[Finite ι]
[(i : ι) → Preorder (π i)]
[(i : ι) → TopologicalSpace (π i)]
[∀ (i : ι), BoundedGENhdsClass (π i)]
:
BoundedGENhdsClass ((i : ι) → π i)
@[instance 100]
instance
OrderTop.to_BoundedLENhdsClass
{α : Type u_2}
[Preorder α]
[TopologicalSpace α]
[OrderTop α]
:
@[instance 100]
instance
OrderBot.to_BoundedGENhdsClass
{α : Type u_2}
[Preorder α]
[TopologicalSpace α]
[OrderBot α]
:
@[instance 100]
instance
BoundedLENhdsClass.of_closedIciTopology
{α : Type u_2}
[LinearOrder α]
[TopologicalSpace α]
[ClosedIciTopology α]
:
@[instance 100]
instance
BoundedGENhdsClass.of_closedIicTopology
{α : Type u_2}
[LinearOrder α]
[TopologicalSpace α]
[ClosedIicTopology α]
:
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)
:
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)
:
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 : Tendsto u f (nhds 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 : Tendsto u f (nhds 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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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).