mathlib documentation

topology.algebra.order.liminf_limsup

Lemmas about liminf and limsup in an order topology. #

theorem filter.tendsto.is_bounded_under_le {α : Type u} {β : Type v} [semilattice_sup α] [topological_space α] [order_topology α] {f : filter β} {u : β → α} {a : α} (h : filter.tendsto u f (nhds a)) :
theorem filter.tendsto.bdd_above_range_of_cofinite {α : Type u} {β : Type v} [semilattice_sup α] [topological_space α] [order_topology α] {u : β → α} {a : α} (h : filter.tendsto u filter.cofinite (nhds a)) :
theorem filter.tendsto.bdd_above_range {α : Type u} [semilattice_sup α] [topological_space α] [order_topology α] {u : → α} {a : α} (h : filter.tendsto u filter.at_top (nhds a)) :
theorem filter.tendsto.is_cobounded_under_ge {α : Type u} {β : Type v} [semilattice_sup α] [topological_space α] [order_topology α] {f : filter β} {u : β → α} {a : α} [f.ne_bot] (h : filter.tendsto u f (nhds a)) :
theorem filter.tendsto.is_bounded_under_le_at_bot {β : Type v} {α : Type u_1} [nonempty α] [preorder α] {f : filter β} {u : β → α} (h : filter.tendsto u f filter.at_bot) :
theorem is_bounded_ge_nhds {α : Type u} [semilattice_inf α] [topological_space α] [order_topology α] (a : α) :
theorem filter.tendsto.is_bounded_under_ge {α : Type u} {β : Type v} [semilattice_inf α] [topological_space α] [order_topology α] {f : filter β} {u : β → α} {a : α} (h : filter.tendsto u f (nhds a)) :
theorem filter.tendsto.bdd_below_range_of_cofinite {α : Type u} {β : Type v} [semilattice_inf α] [topological_space α] [order_topology α] {u : β → α} {a : α} (h : filter.tendsto u filter.cofinite (nhds a)) :
theorem filter.tendsto.bdd_below_range {α : Type u} [semilattice_inf α] [topological_space α] [order_topology α] {u : → α} {a : α} (h : filter.tendsto u filter.at_top (nhds a)) :
theorem filter.tendsto.is_cobounded_under_le {α : Type u} {β : Type v} [semilattice_inf α] [topological_space α] [order_topology α] {f : filter β} {u : β → α} {a : α} [f.ne_bot] (h : filter.tendsto u f (nhds a)) :
theorem is_bounded_ge_at_top (α : Type u_1) [hα : nonempty α] [preorder α] :
theorem filter.tendsto.is_bounded_under_ge_at_top {β : Type v} {α : Type u_1} [nonempty α] [preorder α] {f : filter β} {u : β → α} (h : filter.tendsto u f filter.at_top) :
theorem lt_mem_sets_of_Limsup_lt {α : Type u} [conditionally_complete_linear_order α] {f : filter α} {b : α} (h : filter.is_bounded has_le.le f) (l : f.Limsup < b) :
∀ᶠ (a : α) in f, a < b
theorem gt_mem_sets_of_Liminf_gt {α : Type u} [conditionally_complete_linear_order α] {f : filter α} {b : α} :
filter.is_bounded ge fb < f.Liminf(∀ᶠ (a : α) in f, b < a)
theorem le_nhds_of_Limsup_eq_Liminf {α : Type u} [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) :
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} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] (a : α) :
(nhds a).Limsup = a
theorem Liminf_nhds {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] (a : α) :
(nhds a).Liminf = a
theorem Liminf_eq_of_le_nhds {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] {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} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] {f : filter α} {a : α} [f.ne_bot] :
f nhds af.Limsup = a

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

theorem filter.tendsto.limsup_eq {α : Type u} {β : Type v} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] {f : filter β} {u : β → α} {a : α} [f.ne_bot] (h : filter.tendsto u f (nhds a)) :
f.limsup u = a

If a function has a limit, then its limsup coincides with its limit.

theorem filter.tendsto.liminf_eq {α : Type u} {β : Type v} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] {f : filter β} {u : β → α} {a : α} [f.ne_bot] (h : filter.tendsto u f (nhds a)) :
f.liminf u = a

If a function has a limit, then its liminf coincides with its limit.

theorem tendsto_of_liminf_eq_limsup {α : Type u} {β : Type v} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] {f : filter β} {u : β → α} {a : α} (hinf : f.liminf u = a) (hsup : f.limsup u = 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") :

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} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] {f : filter β} {u : β → α} {a : α} (hinf : a f.liminf u) (hsup : f.limsup u 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") :

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} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [densely_ordered α] {f : filter β} {u : β → α} {s : set α} (hs : dense s) (H : ∀ (a : α), a s∀ (b : α), b sa < 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 antitone.map_Limsup_of_continuous_at {R : Type u_2} {S : Type u_3} [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 = F.liminf 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_2} {S : Type u_3} {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 (F.limsup a)) :
f (F.limsup a) = F.liminf (f a)

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_2} {S : Type u_3} [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 = F.limsup 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_2} {S : Type u_3} {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 (F.liminf a)) :
f (F.liminf a) = F.limsup (f a)

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_2} {S : Type u_3} [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 = F.limsup 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_2} {S : Type u_3} {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 (F.limsup a)) :
f (F.limsup a) = F.limsup (f a)

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_2} {S : Type u_3} [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 = F.liminf 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_2} {S : Type u_3} {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 (F.liminf a)) :
f (F.liminf a) = F.liminf (f a)

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

theorem limsup_eq_tendsto_sum_indicator_nat_at_top {α : Type u} (s : set α) :
filter.at_top.limsup s = {ω : α | 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} (R : Type u_1) [ordered_semiring R] [nontrivial R] [archimedean R] (s : set α) :
filter.at_top.limsup s = {ω : α | filter.tendsto (λ (n : ), (finset.range n).sum (λ (k : ), (s (k + 1)).indicator 1 ω)) filter.at_top filter.at_top}