# Documentation

Mathlib.Topology.Algebra.Order.LiminfLimsup

# Lemmas about liminf and limsup in an order topology. #

theorem isBounded_le_nhds {α : Type u} [] [] [] (a : α) :
Filter.IsBounded (fun x x_1 => x x_1) (nhds a)
theorem Filter.Tendsto.isBoundedUnder_le {α : Type u} {β : Type v} [] [] [] {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} {β : Type v} [] [] [] {u : βα} {a : α} (h : Filter.Tendsto u Filter.cofinite (nhds a)) :
theorem Filter.Tendsto.bddAbove_range {α : Type u} [] [] [] {u : α} {a : α} (h : Filter.Tendsto u Filter.atTop (nhds a)) :
theorem isCobounded_ge_nhds {α : Type u} [] [] [] (a : α) :
Filter.IsCobounded (fun x x_1 => x x_1) (nhds a)
theorem Filter.Tendsto.isCoboundedUnder_ge {α : Type u} {β : Type v} [] [] [] {f : } {u : βα} {a : α} [] (h : Filter.Tendsto u f (nhds a)) :
Filter.IsCoboundedUnder (fun x x_1 => x x_1) f u
theorem isBounded_ge_nhds {α : Type u} [] [] [] (a : α) :
Filter.IsBounded (fun x x_1 => x x_1) (nhds a)
theorem Filter.Tendsto.isBoundedUnder_ge {α : Type u} {β : Type v} [] [] [] {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} {β : Type v} [] [] [] {u : βα} {a : α} (h : Filter.Tendsto u Filter.cofinite (nhds a)) :
theorem Filter.Tendsto.bddBelow_range {α : Type u} [] [] [] {u : α} {a : α} (h : Filter.Tendsto u Filter.atTop (nhds a)) :
theorem isCobounded_le_nhds {α : Type u} [] [] [] (a : α) :
Filter.IsCobounded (fun x x_1 => x x_1) (nhds a)
theorem Filter.Tendsto.isCoboundedUnder_le {α : Type u} {β : Type v} [] [] [] {f : } {u : βα} {a : α} [] (h : Filter.Tendsto u f (nhds a)) :
Filter.IsCoboundedUnder (fun x x_1 => x x_1) f u
theorem le_nhds_of_limsSup_eq_limsInf {α : Type u} [] [] {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} [] [] (a : α) :
= a
theorem limsInf_nhds {α : Type u} [] [] (a : α) :
= a
theorem limsInf_eq_of_le_nhds {α : Type u} [] [] {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} [] [] {f : } {a : α} [] :
f nhds a

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

theorem Filter.Tendsto.limsup_eq {α : Type u} {β : Type v} [] [] {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} {β : Type v} [] [] {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} {β : Type v} [] [] {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} {β : Type v} [] [] {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} {β : Type v} [] [] [] {f : } {u : βα} {s : Set α} (hs : ) (H : ∀ (a : α), a s∀ (b : α), b sa < 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} {β : Type v} [] [] {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} {β : Type v} [] [] {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} {β : Type v} [] [] {f : } {u : βα} :
@[simp]
theorem liminf_eq_top {α : Type u} {β : Type v} [] [] {f : } {u : βα} :
theorem Antitone.map_limsSup_of_continuousAt {R : Type u_2} {S : Type u_3} [] [] [] [] {F : } [] {f : RS} (f_decr : ) (f_cont : ) (bdd_above : autoParam (Filter.IsBounded (fun x x_1 => x x_1) F) _auto✝) (bdd_below : autoParam (Filter.IsBounded (fun x x_1 => 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_2} {S : Type u_3} {F : } [] [] [] [] [] {f : RS} (f_decr : ) (a : ιR) (f_cont : ContinuousAt f ()) (bdd_above : autoParam (Filter.IsBoundedUnder (fun x x_1 => x x_1) F a) _auto✝) (bdd_below : autoParam (Filter.IsBoundedUnder (fun x x_1 => 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_2} {S : Type u_3} [] [] [] [] {F : } [] {f : RS} (f_decr : ) (f_cont : ) (bdd_above : autoParam (Filter.IsBounded (fun x x_1 => x x_1) F) _auto✝) (bdd_below : autoParam (Filter.IsBounded (fun x x_1 => 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_2} {S : Type u_3} {F : } [] [] [] [] [] {f : RS} (f_decr : ) (a : ιR) (f_cont : ContinuousAt f ()) (bdd_above : autoParam (Filter.IsBoundedUnder (fun x x_1 => x x_1) F a) _auto✝) (bdd_below : autoParam (Filter.IsBoundedUnder (fun x x_1 => 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_2} {S : Type u_3} [] [] [] [] {F : } [] {f : RS} (f_incr : ) (f_cont : ) (bdd_above : autoParam (Filter.IsBounded (fun x x_1 => x x_1) F) _auto✝) (bdd_below : autoParam (Filter.IsBounded (fun x x_1 => 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_2} {S : Type u_3} {F : } [] [] [] [] [] {f : RS} (f_incr : ) (a : ιR) (f_cont : ContinuousAt f ()) (bdd_above : autoParam (Filter.IsBoundedUnder (fun x x_1 => x x_1) F a) _auto✝) (bdd_below : autoParam (Filter.IsBoundedUnder (fun x x_1 => 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_2} {S : Type u_3} [] [] [] [] {F : } [] {f : RS} (f_incr : ) (f_cont : ) (bdd_above : autoParam (Filter.IsBounded (fun x x_1 => x x_1) F) _auto✝) (bdd_below : autoParam (Filter.IsBounded (fun x x_1 => 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_2} {S : Type u_3} {F : } [] [] [] [] [] {f : RS} (f_incr : ) (a : ιR) (f_cont : ContinuousAt f ()) (bdd_above : autoParam (Filter.IsBoundedUnder (fun x x_1 => x x_1) F a) _auto✝) (bdd_below : autoParam (Filter.IsBoundedUnder (fun x x_1 => 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_2} [] [] {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_2} [] [] {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 {R : Type u_2} [] [] {ι : Type u_3} (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 {R : Type u_2} [] [] {ι : Type u_3} (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} (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} (R : Type u_1) [] (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 {R : Type u_1} [] [] {ι : Type u_2} (F : ) [] [Add R] [] [CovariantClass R R (fun x y => x + y) fun x y => x y] (f : ιR) (c : R) (bdd_above : Filter.IsBoundedUnder (fun x x_1 => x x_1) F f) (bdd_below : Filter.IsBoundedUnder (fun x x_1 => x x_1) F f) :
Filter.limsup (fun i => c + f i) F = c +

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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