Lemmas about liminf and limsup in an order topology. #
theorem
is_bounded_le_nhds
{α : Type u}
[semilattice_sup α]
[topological_space α]
[order_topology α]
(a : α) :
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 (𝓝 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 (𝓝 a)) :
theorem
filter.tendsto.bdd_above_range
{α : Type u}
[semilattice_sup α]
[topological_space α]
[order_topology α]
{u : ℕ → α}
{a : α}
(h : filter.tendsto u filter.at_top (𝓝 a)) :
theorem
is_cobounded_ge_nhds
{α : Type u}
[semilattice_sup α]
[topological_space α]
[order_topology α]
(a : α) :
filter.is_cobounded ge (𝓝 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 (𝓝 a)) :
theorem
is_bounded_ge_nhds
{α : Type u}
[semilattice_inf α]
[topological_space α]
[order_topology α]
(a : α) :
filter.is_bounded ge (𝓝 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 (𝓝 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 (𝓝 a)) :
theorem
filter.tendsto.bdd_below_range
{α : Type u}
[semilattice_inf α]
[topological_space α]
[order_topology α]
{u : ℕ → α}
{a : α}
(h : filter.tendsto u filter.at_top (𝓝 a)) :
theorem
is_cobounded_le_nhds
{α : Type u}
[semilattice_inf α]
[topological_space α]
[order_topology α]
(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 (𝓝 a)) :
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 f → b < 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) :
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 : α) :
theorem
Liminf_nhds
{α : Type u}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
(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 ≤ 𝓝 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] :
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 (𝓝 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 (𝓝 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") :
filter.tendsto u f (𝓝 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}
{β : 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") :
filter.tendsto u f (𝓝 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}
{β : 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 ∈ 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 (𝓝 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.