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]
- is_bounded_le_nhds : ∀ (a : α), filter.is_bounded has_le.le (nhds a)
Ad hoc typeclass stating that neighborhoods are eventually bounded above.
@[class]
- is_bounded_ge_nhds : ∀ (a : α), filter.is_bounded ge (nhds a)
Ad hoc typeclass stating that neighborhoods are eventually bounded below.
theorem
is_bounded_le_nhds
{α : Type u_2}
[preorder α]
[topological_space α]
[bounded_le_nhds_class α]
(a : α) :
theorem
filter.tendsto.is_bounded_under_le
{ι : Type u_1}
{α : Type u_2}
[preorder α]
[topological_space α]
[bounded_le_nhds_class α]
{f : filter ι}
{u : ι → α}
{a : α}
(h : filter.tendsto u f (nhds a)) :
theorem
filter.tendsto.bdd_above_range_of_cofinite
{ι : Type u_1}
{α : Type u_2}
[preorder α]
[topological_space α]
[bounded_le_nhds_class α]
{u : ι → α}
{a : α}
[is_directed α has_le.le]
(h : filter.tendsto u filter.cofinite (nhds a)) :
theorem
filter.tendsto.bdd_above_range
{α : Type u_2}
[preorder α]
[topological_space α]
[bounded_le_nhds_class α]
{a : α}
[is_directed α has_le.le]
{u : ℕ → α}
(h : filter.tendsto u filter.at_top (nhds a)) :
theorem
is_cobounded_ge_nhds
{α : Type u_2}
[preorder α]
[topological_space α]
[bounded_le_nhds_class α]
(a : α) :
theorem
filter.tendsto.is_cobounded_under_ge
{ι : Type u_1}
{α : Type u_2}
[preorder α]
[topological_space α]
[bounded_le_nhds_class α]
{f : filter ι}
{u : ι → α}
{a : α}
[f.ne_bot]
(h : filter.tendsto u f (nhds a)) :
@[protected, instance]
def
order_dual.bounded_ge_nhds_class
{α : Type u_2}
[preorder α]
[topological_space α]
[bounded_le_nhds_class α] :
@[protected, instance]
def
prod.bounded_le_nhds_class
{α : Type u_2}
{β : Type u_3}
[preorder α]
[preorder β]
[topological_space α]
[topological_space β]
[bounded_le_nhds_class α]
[bounded_le_nhds_class β] :
bounded_le_nhds_class (α × β)
@[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)] :
bounded_le_nhds_class (Π (i : ι), π i)
theorem
is_bounded_ge_nhds
{α : Type u_2}
[preorder α]
[topological_space α]
[bounded_ge_nhds_class α]
(a : α) :
filter.is_bounded ge (nhds a)
theorem
filter.tendsto.is_bounded_under_ge
{ι : Type u_1}
{α : Type u_2}
[preorder α]
[topological_space α]
[bounded_ge_nhds_class α]
{f : filter ι}
{u : ι → α}
{a : α}
(h : filter.tendsto u f (nhds a)) :
theorem
filter.tendsto.bdd_below_range_of_cofinite
{ι : Type u_1}
{α : Type u_2}
[preorder α]
[topological_space α]
[bounded_ge_nhds_class α]
{u : ι → α}
{a : α}
[is_directed α ge]
(h : filter.tendsto u filter.cofinite (nhds a)) :
theorem
filter.tendsto.bdd_below_range
{α : Type u_2}
[preorder α]
[topological_space α]
[bounded_ge_nhds_class α]
{a : α}
[is_directed α ge]
{u : ℕ → α}
(h : filter.tendsto u filter.at_top (nhds a)) :
theorem
is_cobounded_le_nhds
{α : Type u_2}
[preorder α]
[topological_space α]
[bounded_ge_nhds_class α]
(a : α) :
theorem
filter.tendsto.is_cobounded_under_le
{ι : Type u_1}
{α : Type u_2}
[preorder α]
[topological_space α]
[bounded_ge_nhds_class α]
{f : filter ι}
{u : ι → α}
{a : α}
[f.ne_bot]
(h : filter.tendsto u f (nhds a)) :
@[protected, instance]
def
order_dual.bounded_le_nhds_class
{α : Type u_2}
[preorder α]
[topological_space α]
[bounded_ge_nhds_class α] :
@[protected, instance]
def
prod.bounded_ge_nhds_class
{α : Type u_2}
{β : Type u_3}
[preorder α]
[preorder β]
[topological_space α]
[topological_space β]
[bounded_ge_nhds_class α]
[bounded_ge_nhds_class β] :
bounded_ge_nhds_class (α × β)
@[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)] :
bounded_ge_nhds_class (Π (i : ι), π i)
@[protected, instance]
def
order_top.to_bounded_le_nhds_class
{α : Type u_2}
[preorder α]
[topological_space α]
[order_top α] :
@[protected, instance]
def
order_bot.to_bounded_ge_nhds_class
{α : Type u_2}
[preorder α]
[topological_space α]
[order_bot α] :
@[protected, instance]
def
order_topology.to_bounded_le_nhds_class
{α : Type u_2}
[preorder α]
[topological_space α]
[is_directed α has_le.le]
[order_topology α] :
@[protected, instance]
def
order_topology.to_bounded_ge_nhds_class
{α : Type u_2}
[preorder α]
[topological_space α]
[is_directed α ge]
[order_topology α] :
theorem
le_nhds_of_Limsup_eq_Liminf
{α : Type u_2}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
{f : filter α}
{a : α}
(hl : filter.is_bounded has_le.le f)
(hg : filter.is_bounded ge f)
(hs : f.Limsup = a)
(hi : f.Liminf = 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}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
(a : α) :
theorem
Liminf_nhds
{α : Type u_2}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
(a : α) :
theorem
Liminf_eq_of_le_nhds
{α : Type u_2}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
{f : filter α}
{a : α}
[f.ne_bot]
(h : f ≤ nhds a) :
If a filter is converging, its limsup coincides with its limit.
theorem
Limsup_eq_of_le_nhds
{α : Type u_2}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
{f : filter α}
{a : α}
[f.ne_bot] :
If a filter is converging, its liminf coincides with its limit.
theorem
filter.tendsto.limsup_eq
{α : Type u_2}
{β : Type u_3}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
{f : filter β}
{u : β → α}
{a : α}
[f.ne_bot]
(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}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
{f : filter β}
{u : β → α}
{a : α}
[f.ne_bot]
(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}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
{f : filter β}
{u : β → α}
{a : α}
(hinf : filter.liminf u f = a)
(hsup : filter.limsup u f = a)
(h : filter.is_bounded_under has_le.le f u . "is_bounded_default")
(h' : filter.is_bounded_under ge f u . "is_bounded_default") :
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}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
{f : filter β}
{u : β → α}
{a : α}
(hinf : a ≤ filter.liminf u f)
(hsup : filter.limsup u f ≤ a)
(h : filter.is_bounded_under has_le.le f u . "is_bounded_default")
(h' : filter.is_bounded_under ge f u . "is_bounded_default") :
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}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
[densely_ordered α]
{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 : filter.is_bounded_under has_le.le f u . "is_bounded_default")
(h' : filter.is_bounded_under ge f u . "is_bounded_default") :
∃ (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}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
[topological_space.first_countable_topology α]
{f : filter β}
[countable_Inter_filter f]
{u : β → α}
(hf : filter.is_bounded_under has_le.le f u . "is_bounded_default") :
∀ᶠ (b : β) in f, u b ≤ filter.limsup u f
theorem
eventually_liminf_le
{α : Type u_2}
{β : Type u_3}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
[topological_space.first_countable_topology α]
{f : filter β}
[countable_Inter_filter f]
{u : β → α}
(hf : filter.is_bounded_under ge f u . "is_bounded_default") :
∀ᶠ (b : β) in f, filter.liminf u f ≤ u b
@[simp]
theorem
limsup_eq_bot
{α : Type u_2}
{β : Type u_3}
[complete_linear_order α]
[topological_space α]
[topological_space.first_countable_topology α]
[order_topology α]
{f : filter β}
[countable_Inter_filter f]
{u : β → α} :
@[simp]
theorem
liminf_eq_top
{α : Type u_2}
{β : Type u_3}
[complete_linear_order α]
[topological_space α]
[topological_space.first_countable_topology α]
[order_topology α]
{f : filter β}
[countable_Inter_filter f]
{u : β → α} :
theorem
antitone.map_Limsup_of_continuous_at
{R : Type u_4}
{S : Type u_5}
[complete_linear_order R]
[topological_space R]
[order_topology R]
[complete_linear_order S]
[topological_space S]
[order_topology S]
{F : filter R}
[F.ne_bot]
{f : R → S}
(f_decr : antitone f)
(f_cont : continuous_at f F.Limsup) :
f F.Limsup = filter.liminf f F
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]
[complete_linear_order R]
[topological_space R]
[order_topology R]
[complete_linear_order S]
[topological_space S]
[order_topology S]
{f : R → S}
(f_decr : antitone f)
(a : ι → R)
(f_cont : continuous_at f (filter.limsup a F)) :
f (filter.limsup a 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}
[complete_linear_order R]
[topological_space R]
[order_topology R]
[complete_linear_order S]
[topological_space S]
[order_topology S]
{F : filter R}
[F.ne_bot]
{f : R → S}
(f_decr : antitone f)
(f_cont : continuous_at f F.Liminf) :
f F.Liminf = filter.limsup f F
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]
[complete_linear_order R]
[topological_space R]
[order_topology R]
[complete_linear_order S]
[topological_space S]
[order_topology S]
{f : R → S}
(f_decr : antitone f)
(a : ι → R)
(f_cont : continuous_at f (filter.liminf a F)) :
f (filter.liminf a 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}
[complete_linear_order R]
[topological_space R]
[order_topology R]
[complete_linear_order S]
[topological_space S]
[order_topology S]
{F : filter R}
[F.ne_bot]
{f : R → S}
(f_incr : monotone f)
(f_cont : continuous_at f F.Limsup) :
f F.Limsup = filter.limsup f F
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]
[complete_linear_order R]
[topological_space R]
[order_topology R]
[complete_linear_order S]
[topological_space S]
[order_topology S]
{f : R → S}
(f_incr : monotone f)
(a : ι → R)
(f_cont : continuous_at f (filter.limsup a F)) :
f (filter.limsup a 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}
[complete_linear_order R]
[topological_space R]
[order_topology R]
[complete_linear_order S]
[topological_space S]
[order_topology S]
{F : filter R}
[F.ne_bot]
{f : R → S}
(f_incr : monotone f)
(f_cont : continuous_at f F.Liminf) :
f F.Liminf = filter.liminf f F
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]
[complete_linear_order R]
[topological_space R]
[order_topology R]
[complete_linear_order S]
[topological_space S]
[order_topology S]
{f : R → S}
(f_incr : monotone f)
(a : ι → R)
(f_cont : continuous_at f (filter.liminf a F)) :
f (filter.liminf a 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}
[complete_linear_order R]
[topological_space R]
[order_topology R]
{x : R}
{as : ι → R}
(x_le : ∀ (i : ι), x ≤ as i)
{F : filter ι}
[F.ne_bot]
(as_lim : filter.tendsto as F (nhds x)) :
theorem
supr_eq_of_forall_le_of_tendsto
{ι : Type u_1}
{R : Type u_4}
[complete_linear_order R]
[topological_space R]
[order_topology R]
{x : R}
{as : ι → R}
(le_x : ∀ (i : ι), as i ≤ x)
{F : filter ι}
[F.ne_bot]
(as_lim : filter.tendsto as F (nhds x)) :
theorem
Union_Ici_eq_Ioi_of_lt_of_tendsto
{ι : Type u_1}
{R : Type u_4}
[complete_linear_order R]
[topological_space R]
[order_topology R]
(x : R)
{as : ι → R}
(x_lt : ∀ (i : ι), x < as i)
{F : filter ι}
[F.ne_bot]
(as_lim : filter.tendsto as F (nhds x)) :
theorem
Union_Iic_eq_Iio_of_lt_of_tendsto
{ι : Type u_1}
{R : Type u_4}
[complete_linear_order R]
[topological_space R]
[order_topology R]
(x : R)
{as : ι → R}
(lt_x : ∀ (i : ι), as i < x)
{F : filter ι}
[F.ne_bot]
(as_lim : filter.tendsto as F (nhds x)) :
theorem
limsup_eq_tendsto_sum_indicator_nat_at_top
{α : Type u_2}
(s : ℕ → set α) :
filter.limsup s filter.at_top = {ω : α | 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)
[strict_ordered_semiring R]
[archimedean R]
(s : ℕ → set α) :
filter.limsup s filter.at_top = {ω : α | filter.tendsto (λ (n : ℕ), (finset.range n).sum (λ (k : ℕ), (s (k + 1)).indicator 1 ω)) filter.at_top filter.at_top}