# 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.

class BoundedLENhdsClass (α : Type u_7) [] [] :

Ad hoc typeclass stating that neighborhoods are eventually bounded above.

Instances
class BoundedGENhdsClass (α : Type u_7) [] [] :

Ad hoc typeclass stating that neighborhoods are eventually bounded below.

Instances
theorem isBounded_le_nhds {α : Type u_2} [] [] (a : α) :
Filter.IsBounded (fun (x x_1 : α) => x x_1) (nhds a)
theorem Filter.Tendsto.isBoundedUnder_le {ι : Type u_1} {α : Type u_2} [] [] {f : } {u : ια} {a : α} (h : Filter.Tendsto u f (nhds a)) :
Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) f u
theorem Filter.Tendsto.bddAbove_range_of_cofinite {ι : Type u_1} {α : Type u_2} [] [] {u : ια} {a : α} [IsDirected α fun (x x_1 : α) => x x_1] (h : Filter.Tendsto u Filter.cofinite (nhds a)) :
theorem Filter.Tendsto.bddAbove_range {α : Type u_2} [] [] {a : α} [IsDirected α fun (x x_1 : α) => x x_1] {u : α} (h : Filter.Tendsto u Filter.atTop (nhds a)) :
theorem isCobounded_ge_nhds {α : Type u_2} [] [] (a : α) :
Filter.IsCobounded (fun (x x_1 : α) => x x_1) (nhds a)
theorem Filter.Tendsto.isCoboundedUnder_ge {ι : Type u_1} {α : Type u_2} [] [] {f : } {u : ια} {a : α} [] (h : Filter.Tendsto u f (nhds a)) :
Filter.IsCoboundedUnder (fun (x x_1 : α) => x x_1) f u
Equations
• (_ : ) = (_ : )
instance Prod.instBoundedLENhdsClass {α : Type u_2} {β : Type u_3} [] [] [] [] :
Equations
instance Pi.instBoundedLENhdsClass {ι : Type u_1} {π : ιType u_6} [] [(i : ι) → Preorder (π i)] [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), BoundedLENhdsClass (π i)] :
BoundedLENhdsClass ((i : ι) → π i)
Equations
theorem isBounded_ge_nhds {α : Type u_2} [] [] (a : α) :
Filter.IsBounded (fun (x x_1 : α) => x x_1) (nhds a)
theorem Filter.Tendsto.isBoundedUnder_ge {ι : Type u_1} {α : Type u_2} [] [] {f : } {u : ια} {a : α} (h : Filter.Tendsto u f (nhds a)) :
Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) f u
theorem Filter.Tendsto.bddBelow_range_of_cofinite {ι : Type u_1} {α : Type u_2} [] [] {u : ια} {a : α} [IsDirected α fun (x x_1 : α) => x x_1] (h : Filter.Tendsto u Filter.cofinite (nhds a)) :
theorem Filter.Tendsto.bddBelow_range {α : Type u_2} [] [] {a : α} [IsDirected α fun (x x_1 : α) => x x_1] {u : α} (h : Filter.Tendsto u Filter.atTop (nhds a)) :
theorem isCobounded_le_nhds {α : Type u_2} [] [] (a : α) :
Filter.IsCobounded (fun (x x_1 : α) => x x_1) (nhds a)
theorem Filter.Tendsto.isCoboundedUnder_le {ι : Type u_1} {α : Type u_2} [] [] {f : } {u : ια} {a : α} [] (h : Filter.Tendsto u f (nhds a)) :
Filter.IsCoboundedUnder (fun (x x_1 : α) => x x_1) f u
Equations
• (_ : ) = (_ : )
instance Prod.instBoundedGENhdsClass {α : Type u_2} {β : Type u_3} [] [] [] [] :
Equations
instance Pi.instBoundedGENhdsClass {ι : Type u_1} {π : ιType u_6} [] [(i : ι) → Preorder (π i)] [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), BoundedGENhdsClass (π i)] :
BoundedGENhdsClass ((i : ι) → π i)
Equations
instance OrderTop.to_BoundedLENhdsClass {α : Type u_2} [] [] [] :
Equations
• (_ : ) = (_ : )
instance OrderBot.to_BoundedGENhdsClass {α : Type u_2} [] [] [] :
Equations
• (_ : ) = (_ : )
instance OrderTopology.to_BoundedLENhdsClass {α : Type u_2} [] [] [IsDirected α fun (x x_1 : α) => x x_1] [] :
Equations
• (_ : ) = (_ : )
instance OrderTopology.to_BoundedGENhdsClass {α : Type u_2} [] [] [IsDirected α fun (x x_1 : α) => x x_1] [] :
Equations
• (_ : ) = (_ : )
theorem le_nhds_of_limsSup_eq_limsInf {α : Type u_2} [] [] {f : } {a : α} (hl : Filter.IsBounded (fun (x x_1 : α) => x x_1) f) (hg : Filter.IsBounded (fun (x x_1 : α) => x x_1) f) (hs : ) (hi : ) :
f nhds 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} [] [] (a : α) :
= a
theorem limsInf_nhds {α : Type u_2} [] [] (a : α) :
= a
theorem limsInf_eq_of_le_nhds {α : Type u_2} [] [] {f : } {a : α} [] (h : f nhds a) :

If a filter is converging, its limsup coincides with its limit.

theorem limsSup_eq_of_le_nhds {α : Type u_2} [] [] {f : } {a : α} [] :
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} [] [] {f : } {u : βα} {a : α} [] (h : Filter.Tendsto u f (nhds a)) :
= 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} [] [] {f : } {u : βα} {a : α} [] (h : Filter.Tendsto u f (nhds a)) :
= 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} [] [] {f : } {u : βα} {a : α} (hinf : = a) (hsup : = a) (h : autoParam (Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) f u) _auto✝) (h' : autoParam (Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) f u) _auto✝) :

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} [] [] {f : } {u : βα} {a : α} (hinf : a ) (hsup : a) (h : autoParam (Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) f u) _auto✝) (h' : autoParam (Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) f u) _auto✝) :

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} [] [] [] {f : } {u : βα} {s : Set α} (hs : ) (H : as, bs, a < b¬((∃ᶠ (n : β) in f, u n < a) ∃ᶠ (n : β) in f, b < u n)) (h : autoParam (Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) f u) _auto✝) (h' : autoParam (Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) f u) _auto✝) :
∃ (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} [] [] {f : } {u : βα} (hf : autoParam (Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) f u) _auto✝) :
∀ᶠ (b : β) in f, u b
theorem eventually_liminf_le {α : Type u_2} {β : Type u_3} [] [] {f : } {u : βα} (hf : autoParam (Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) f u) _auto✝) :
∀ᶠ (b : β) in f, u b
@[simp]
theorem limsup_eq_bot {α : Type u_2} {β : Type u_3} [] [] {f : } {u : βα} :
@[simp]
theorem liminf_eq_top {α : Type u_2} {β : Type u_3} [] [] {f : } {u : βα} :
theorem Antitone.map_limsSup_of_continuousAt {R : Type u_4} {S : Type u_5} [] [] [] [] {F : } [] {f : RS} (f_decr : ) (f_cont : ) (bdd_above : autoParam (Filter.IsBounded (fun (x x_1 : R) => x x_1) F) _auto✝) (bdd_below : autoParam (Filter.IsBounded (fun (x x_1 : R) => x x_1) F) _auto✝) :
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 below).

theorem Antitone.map_limsup_of_continuousAt {ι : Type u_1} {R : Type u_4} {S : Type u_5} {F : } [] [] [] [] [] {f : RS} (f_decr : ) (a : ιR) (f_cont : ContinuousAt f ()) (bdd_above : autoParam (Filter.IsBoundedUnder (fun (x x_1 : R) => x x_1) F a) _auto✝) (bdd_below : autoParam (Filter.IsBoundedUnder (fun (x x_1 : R) => x x_1) F a) _auto✝) :
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 below).

theorem Antitone.map_limsInf_of_continuousAt {R : Type u_4} {S : Type u_5} [] [] [] [] {F : } [] {f : RS} (f_decr : ) (f_cont : ) (bdd_above : autoParam (Filter.IsBounded (fun (x x_1 : R) => x x_1) F) _auto✝) (bdd_below : autoParam (Filter.IsBounded (fun (x x_1 : R) => x x_1) F) _auto✝) :
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 above and below).

theorem Antitone.map_liminf_of_continuousAt {ι : Type u_1} {R : Type u_4} {S : Type u_5} {F : } [] [] [] [] [] {f : RS} (f_decr : ) (a : ιR) (f_cont : ContinuousAt f ()) (bdd_above : autoParam (Filter.IsBoundedUnder (fun (x x_1 : R) => x x_1) F a) _auto✝) (bdd_below : autoParam (Filter.IsBoundedUnder (fun (x x_1 : R) => x x_1) F a) _auto✝) :
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 above and below).

theorem Monotone.map_limsSup_of_continuousAt {R : Type u_4} {S : Type u_5} [] [] [] [] {F : } [] {f : RS} (f_incr : ) (f_cont : ) (bdd_above : autoParam (Filter.IsBounded (fun (x x_1 : R) => x x_1) F) _auto✝) (bdd_below : autoParam (Filter.IsBounded (fun (x x_1 : R) => x x_1) F) _auto✝) :
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 below).

theorem Monotone.map_limsup_of_continuousAt {ι : Type u_1} {R : Type u_4} {S : Type u_5} {F : } [] [] [] [] [] {f : RS} (f_incr : ) (a : ιR) (f_cont : ContinuousAt f ()) (bdd_above : autoParam (Filter.IsBoundedUnder (fun (x x_1 : R) => x x_1) F a) _auto✝) (bdd_below : autoParam (Filter.IsBoundedUnder (fun (x x_1 : R) => x x_1) F a) _auto✝) :
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 below).

theorem Monotone.map_limsInf_of_continuousAt {R : Type u_4} {S : Type u_5} [] [] [] [] {F : } [] {f : RS} (f_incr : ) (f_cont : ) (bdd_above : autoParam (Filter.IsBounded (fun (x x_1 : R) => x x_1) F) _auto✝) (bdd_below : autoParam (Filter.IsBounded (fun (x x_1 : R) => x x_1) F) _auto✝) :
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 above and below).

theorem Monotone.map_liminf_of_continuousAt {ι : Type u_1} {R : Type u_4} {S : Type u_5} {F : } [] [] [] [] [] {f : RS} (f_incr : ) (a : ιR) (f_cont : ContinuousAt f ()) (bdd_above : autoParam (Filter.IsBoundedUnder (fun (x x_1 : R) => x x_1) F a) _auto✝) (bdd_below : autoParam (Filter.IsBoundedUnder (fun (x x_1 : R) => x x_1) F a) _auto✝) :
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 above and below).

theorem iInf_eq_of_forall_le_of_tendsto {ι : Type u_1} {R : Type u_4} [] [] {x : R} {as : ιR} (x_le : ∀ (i : ι), x as i) {F : } [] (as_lim : Filter.Tendsto as F (nhds x)) :
⨅ (i : ι), as i = x
theorem iSup_eq_of_forall_le_of_tendsto {ι : Type u_1} {R : Type u_4} [] [] {x : R} {as : ιR} (le_x : ∀ (i : ι), as i x) {F : } [] (as_lim : Filter.Tendsto as F (nhds x)) :
⨆ (i : ι), as i = x
theorem iUnion_Ici_eq_Ioi_of_lt_of_tendsto {ι : Type u_1} {R : Type u_4} [] [] (x : R) {as : ιR} (x_lt : ∀ (i : ι), x < as i) {F : } [] (as_lim : Filter.Tendsto as F (nhds x)) :
⋃ (i : ι), Set.Ici (as i) =
theorem iUnion_Iic_eq_Iio_of_lt_of_tendsto {ι : Type u_1} {R : Type u_4} [] [] (x : R) {as : ιR} (lt_x : ∀ (i : ι), as i < x) {F : } [] (as_lim : Filter.Tendsto as F (nhds x)) :
⋃ (i : ι), Set.Iic (as i) =
theorem limsup_eq_tendsto_sum_indicator_nat_atTop {α : Type u_2} (s : Set α) :
Filter.limsup s Filter.atTop = {ω : α | Filter.Tendsto (fun (n : ) => Finset.sum () fun (k : ) => Set.indicator (s (k + 1)) 1 ω) Filter.atTop Filter.atTop}
theorem limsup_eq_tendsto_sum_indicator_atTop {α : Type u_2} (R : Type u_7) [] (s : Set α) :
Filter.limsup s Filter.atTop = {ω : α | Filter.Tendsto (fun (n : ) => Finset.sum () fun (k : ) => Set.indicator (s (k + 1)) 1 ω) Filter.atTop Filter.atTop}
theorem limsup_const_add {ι : Type u_1} {R : Type u_4} [] [] (F : ) [] [Add R] [] [CovariantClass R R (fun (x y : R) => x + y) fun (x y : R) => x y] (f : ιR) (c : R) (bdd_above : Filter.IsBoundedUnder (fun (x x_1 : R) => x x_1) F f) (bdd_below : Filter.IsBoundedUnder (fun (x x_1 : R) => x x_1) F f) :
Filter.limsup (fun (i : ι) => c + f i) F = c +

liminf (c + xᵢ) = c + liminf xᵢ.

theorem limsup_add_const {ι : Type u_1} {R : Type u_4} [] [] (F : ) [] [Add R] [] [CovariantClass R R (Function.swap fun (x y : R) => x + y) fun (x y : R) => x y] (f : ιR) (c : R) (bdd_above : Filter.IsBoundedUnder (fun (x x_1 : R) => x x_1) F f) (bdd_below : Filter.IsBoundedUnder (fun (x x_1 : R) => x x_1) F f) :
Filter.limsup (fun (i : ι) => f i + c) F = + c

limsup (xᵢ + c) = (limsup xᵢ) + c.

theorem liminf_const_add {ι : Type u_1} {R : Type u_4} [] [] (F : ) [] [Add R] [] [CovariantClass R R (fun (x y : R) => x + y) fun (x y : R) => x y] (f : ιR) (c : R) (bdd_above : Filter.IsBoundedUnder (fun (x x_1 : R) => x x_1) F f) (bdd_below : Filter.IsBoundedUnder (fun (x x_1 : R) => x x_1) F f) :
Filter.liminf (fun (i : ι) => c + f i) F = c +

liminf (c + xᵢ) = c + limsup xᵢ.

theorem liminf_add_const {ι : Type u_1} {R : Type u_4} [] [] (F : ) [] [Add R] [] [CovariantClass R R (Function.swap fun (x y : R) => x + y) fun (x y : R) => x y] (f : ιR) (c : R) (bdd_above : Filter.IsBoundedUnder (fun (x x_1 : R) => x x_1) F f) (bdd_below : Filter.IsBoundedUnder (fun (x x_1 : R) => x x_1) F f) :
Filter.liminf (fun (i : ι) => f i + c) F = + c

liminf (xᵢ + c) = (liminf xᵢ) + c.

theorem limsup_const_sub {ι : Type u_1} {R : Type u_4} [] [] (F : ) [] [] [Sub R] [] [] [CovariantClass R R (fun (x y : R) => x + y) fun (x y : R) => x y] (f : ιR) (c : R) (bdd_above : Filter.IsBoundedUnder (fun (x x_1 : R) => x x_1) F f) (bdd_below : Filter.IsBoundedUnder (fun (x x_1 : R) => x x_1) F f) :
Filter.limsup (fun (i : ι) => c - f i) F = c -

limsup (c - xᵢ) = c - liminf xᵢ.

theorem limsup_sub_const {ι : Type u_1} {R : Type u_4} [] [] (F : ) [] [] [Sub R] [] [] (f : ιR) (c : R) (bdd_above : Filter.IsBoundedUnder (fun (x x_1 : R) => x x_1) F f) (bdd_below : Filter.IsBoundedUnder (fun (x x_1 : R) => x x_1) F f) :
Filter.limsup (fun (i : ι) => f i - c) F = - c

limsup (xᵢ - c) = (limsup xᵢ) - c.

theorem liminf_const_sub {ι : Type u_1} {R : Type u_4} [] [] (F : ) [] [] [Sub R] [] [] [CovariantClass R R (fun (x y : R) => x + y) fun (x y : R) => x y] (f : ιR) (c : R) (bdd_above : Filter.IsBoundedUnder (fun (x x_1 : R) => x x_1) F f) (bdd_below : Filter.IsBoundedUnder (fun (x x_1 : R) => x x_1) F f) :
Filter.liminf (fun (i : ι) => c - f i) F = c -

liminf (c - xᵢ) = c - limsup xᵢ.

theorem liminf_sub_const {ι : Type u_1} {R : Type u_4} [] [] (F : ) [] [] [Sub R] [] [] (f : ιR) (c : R) (bdd_above : Filter.IsBoundedUnder (fun (x x_1 : R) => x x_1) F f) (bdd_below : Filter.IsBoundedUnder (fun (x x_1 : R) => x x_1) F f) :
Filter.liminf (fun (i : ι) => f i - c) F = - c

liminf (xᵢ - c) = (liminf xᵢ) - c.