mathlib3documentation

topology.algebra.order.liminf_limsup

Lemmas about liminf and limsup in an order topology. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Main declarations #

• bounded_le_nhds_class: Typeclass stating that neighborhoods are eventually bounded above.
• bounded_ge_nhds_class: Typeclass stating that neighborhoods are eventually bounded below.

Implementation notes #

The same lemmas are true in ℝ, ℝ × ℝ, ι → ℝ, euclidean_space ι ℝ. To avoid code duplication, we provide an ad hoc axiomatisation of the properties we need.

@[class]
structure bounded_le_nhds_class (α : Type u_7) [preorder α]  :
Prop
• is_bounded_le_nhds : (a : α),

Ad hoc typeclass stating that neighborhoods are eventually bounded above.

Instances of this typeclass
@[class]
structure bounded_ge_nhds_class (α : Type u_7) [preorder α]  :
Prop
• is_bounded_ge_nhds : (a : α),

Ad hoc typeclass stating that neighborhoods are eventually bounded below.

Instances of this typeclass
theorem is_bounded_le_nhds {α : Type u_2} [preorder α] (a : α) :
theorem filter.tendsto.is_bounded_under_le {ι : Type u_1} {α : Type u_2} [preorder α] {f : filter ι} {u : ι α} {a : α} (h : (nhds a)) :
theorem filter.tendsto.bdd_above_range_of_cofinite {ι : Type u_1} {α : Type u_2} [preorder α] {u : ι α} {a : α} (h : (nhds a)) :
theorem filter.tendsto.bdd_above_range {α : Type u_2} [preorder α] {a : α} {u : α} (h : (nhds a)) :
theorem is_cobounded_ge_nhds {α : Type u_2} [preorder α] (a : α) :
theorem filter.tendsto.is_cobounded_under_ge {ι : Type u_1} {α : Type u_2} [preorder α] {f : filter ι} {u : ι α} {a : α} [f.ne_bot] (h : (nhds a)) :
@[protected, instance]
@[protected, instance]
def prod.bounded_le_nhds_class {α : Type u_2} {β : Type u_3} [preorder α] [preorder β]  :
@[protected, instance]
def pi.bounded_le_nhds_class {ι : Type u_1} {π : ι Type u_6} [finite ι] [Π (i : ι), preorder (π i)] [Π (i : ι), topological_space (π i)] [ (i : ι), ] :
bounded_le_nhds_class (Π (i : ι), π i)
theorem is_bounded_ge_nhds {α : Type u_2} [preorder α] (a : α) :
theorem filter.tendsto.is_bounded_under_ge {ι : Type u_1} {α : Type u_2} [preorder α] {f : filter ι} {u : ι α} {a : α} (h : (nhds a)) :
theorem filter.tendsto.bdd_below_range_of_cofinite {ι : Type u_1} {α : Type u_2} [preorder α] {u : ι α} {a : α} [ ge] (h : (nhds a)) :
theorem filter.tendsto.bdd_below_range {α : Type u_2} [preorder α] {a : α} [ ge] {u : α} (h : (nhds a)) :
theorem is_cobounded_le_nhds {α : Type u_2} [preorder α] (a : α) :
theorem filter.tendsto.is_cobounded_under_le {ι : Type u_1} {α : Type u_2} [preorder α] {f : filter ι} {u : ι α} {a : α} [f.ne_bot] (h : (nhds a)) :
@[protected, instance]
@[protected, instance]
def prod.bounded_ge_nhds_class {α : Type u_2} {β : Type u_3} [preorder α] [preorder β]  :
@[protected, instance]
def pi.bounded_ge_nhds_class {ι : Type u_1} {π : ι Type u_6} [finite ι] [Π (i : ι), preorder (π i)] [Π (i : ι), topological_space (π i)] [ (i : ι), ] :
bounded_ge_nhds_class (Π (i : ι), π i)
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
theorem le_nhds_of_Limsup_eq_Liminf {α : Type u_2} {f : filter α} {a : α} (hl : f) (hg : f) (hs : f.Limsup = a) (hi : f.Liminf = a) :
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 Limsup_nhds {α : Type u_2} (a : α) :
(nhds a).Limsup = a
theorem Liminf_nhds {α : Type u_2} (a : α) :
(nhds a).Liminf = a
theorem Liminf_eq_of_le_nhds {α : Type u_2} {f : filter α} {a : α} [f.ne_bot] (h : f nhds a) :
f.Liminf = a

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

theorem Limsup_eq_of_le_nhds {α : Type u_2} {f : filter α} {a : α} [f.ne_bot] :
f nhds a f.Limsup = a

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

theorem filter.tendsto.limsup_eq {α : Type u_2} {β : Type u_3} {f : filter β} {u : β α} {a : α} [f.ne_bot] (h : (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 : filter β} {u : β α} {a : α} [f.ne_bot] (h : (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 : filter β} {u : β α} {a : α} (hinf : = a) (hsup : = a) (h : . "is_bounded_default") (h' : . "is_bounded_default") :
(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} {f : filter β} {u : β α} {a : α} (hinf : a ) (hsup : a) (h : . "is_bounded_default") (h' : . "is_bounded_default") :
(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} {f : filter β} {u : β α} {s : set α} (hs : dense s) (H : (a : α), a s (b : α), b s a < b ¬((∃ᶠ (n : β) in f, u n < a) ∃ᶠ (n : β) in f, b < u n)) (h : . "is_bounded_default") (h' : . "is_bounded_default") :
(c : α), (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 : filter β} {u : β α} (hf : . "is_bounded_default") :
∀ᶠ (b : β) in f, u b
theorem eventually_liminf_le {α : Type u_2} {β : Type u_3} {f : filter β} {u : β α} (hf : . "is_bounded_default") :
∀ᶠ (b : β) in f, u b
@[simp]
theorem limsup_eq_bot {α : Type u_2} {β : Type u_3} {f : filter β} {u : β α} :
@[simp]
theorem liminf_eq_top {α : Type u_2} {β : Type u_3} {f : filter β} {u : β α} :
theorem antitone.map_Limsup_of_continuous_at {R : Type u_4} {S : Type u_5} {F : filter R} [F.ne_bot] {f : R S} (f_decr : antitone f) (f_cont : F.Limsup) :
f F.Limsup =

An antitone function between complete linear ordered spaces sends a filter.Limsup to the filter.liminf of the image if it is continuous at the Limsup.

theorem antitone.map_limsup_of_continuous_at {ι : Type u_1} {R : Type u_4} {S : Type u_5} {F : filter ι} [F.ne_bot] {f : R S} (f_decr : antitone f) (a : ι R) (f_cont : F)) :
f F) = filter.liminf (f a) F

A continuous antitone function between complete linear ordered spaces sends a filter.limsup to the filter.liminf of the images.

theorem antitone.map_Liminf_of_continuous_at {R : Type u_4} {S : Type u_5} {F : filter R} [F.ne_bot] {f : R S} (f_decr : antitone f) (f_cont : F.Liminf) :
f F.Liminf =

An antitone function between complete linear ordered spaces sends a filter.Liminf to the filter.limsup of the image if it is continuous at the Liminf.

theorem antitone.map_liminf_of_continuous_at {ι : Type u_1} {R : Type u_4} {S : Type u_5} {F : filter ι} [F.ne_bot] {f : R S} (f_decr : antitone f) (a : ι R) (f_cont : F)) :
f F) = filter.limsup (f a) F

A continuous antitone function between complete linear ordered spaces sends a filter.liminf to the filter.limsup of the images.

theorem monotone.map_Limsup_of_continuous_at {R : Type u_4} {S : Type u_5} {F : filter R} [F.ne_bot] {f : R S} (f_incr : monotone f) (f_cont : F.Limsup) :
f F.Limsup =

A monotone function between complete linear ordered spaces sends a filter.Limsup to the filter.limsup of the image if it is continuous at the Limsup.

theorem monotone.map_limsup_of_continuous_at {ι : Type u_1} {R : Type u_4} {S : Type u_5} {F : filter ι} [F.ne_bot] {f : R S} (f_incr : monotone f) (a : ι R) (f_cont : F)) :
f F) = filter.limsup (f a) F

A continuous monotone function between complete linear ordered spaces sends a filter.limsup to the filter.limsup of the images.

theorem monotone.map_Liminf_of_continuous_at {R : Type u_4} {S : Type u_5} {F : filter R} [F.ne_bot] {f : R S} (f_incr : monotone f) (f_cont : F.Liminf) :
f F.Liminf =

A monotone function between complete linear ordered spaces sends a filter.Liminf to the filter.liminf of the image if it is continuous at the Liminf.

theorem monotone.map_liminf_of_continuous_at {ι : Type u_1} {R : Type u_4} {S : Type u_5} {F : filter ι} [F.ne_bot] {f : R S} (f_incr : monotone f) (a : ι R) (f_cont : F)) :
f F) = filter.liminf (f a) F

A continuous monotone function between complete linear ordered spaces sends a filter.liminf to the filter.liminf of the images.

theorem infi_eq_of_forall_le_of_tendsto {ι : Type u_1} {R : Type u_4} {x : R} {as : ι R} (x_le : (i : ι), x as i) {F : filter ι} [F.ne_bot] (as_lim : F (nhds x)) :
( (i : ι), as i) = x
theorem supr_eq_of_forall_le_of_tendsto {ι : Type u_1} {R : Type u_4} {x : R} {as : ι R} (le_x : (i : ι), as i x) {F : filter ι} [F.ne_bot] (as_lim : F (nhds x)) :
( (i : ι), as i) = x
theorem Union_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 : filter ι} [F.ne_bot] (as_lim : F (nhds x)) :
( (i : ι), set.Ici (as i)) =
theorem Union_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 : filter ι} [F.ne_bot] (as_lim : F (nhds x)) :
( (i : ι), set.Iic (as i)) =
theorem limsup_eq_tendsto_sum_indicator_nat_at_top {α : Type u_2} (s : set α) :
= {ω : α | filter.tendsto (λ (n : ), (finset.range n).sum (λ (k : ), (s (k + 1)).indicator 1 ω)) filter.at_top filter.at_top}
theorem limsup_eq_tendsto_sum_indicator_at_top {α : Type u_2} (R : Type u_1) [archimedean R] (s : set α) :
= {ω : α | filter.tendsto (λ (n : ), (finset.range n).sum (λ (k : ), (s (k + 1)).indicator 1 ω)) filter.at_top filter.at_top}