Bounded monotone sequences converge #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file we prove a few theorems of the form “if the range of a monotone function f : ι → α
admits a least upper bound a, then f x tends to a as x → ∞”, as well as version of this
statement for (conditionally) complete lattices that use ⨆ x, f x instead of is_lub.
These theorems work for linear orders with order topologies as well as their products (both in terms
of prod and in terms of function types). In order to reduce code duplication, we introduce two
typeclasses (one for the property formulated above and one for the dual property), prove theorems
assuming one of these typeclasses, and provide instances for linear orders and their products.
We also prove some "inverse" results: if f n is a monotone sequence and a is its limit,
then f n ≤ a for all n.
Tags #
monotone convergence
@[class]
- tendsto_coe_at_top_is_lub : ∀ (a : α) (s : set α), is_lub s a → filter.tendsto coe filter.at_top (nhds a)
We say that α is a Sup_convergence_class if the following holds. Let f : ι → α be a
monotone function, let a : α be a least upper bound of set.range f. Then f x tends to 𝓝 a as
x → ∞ (formally, at the filter filter.at_top). We require this for ι = (s : set α), f = coe
in the definition, then prove it for any f in tendsto_at_top_is_lub.
This property holds for linear orders with order topology as well as their products.
@[class]
- tendsto_coe_at_bot_is_glb : ∀ (a : α) (s : set α), is_glb s a → filter.tendsto coe filter.at_bot (nhds a)
We say that α is an Inf_convergence_class if the following holds. Let f : ι → α be a
monotone function, let a : α be a greatest lower bound of set.range f. Then f x tends to 𝓝 a
as x → -∞ (formally, at the filter filter.at_bot). We require this for ι = (s : set α),
f = coe in the definition, then prove it for any f in tendsto_at_bot_is_glb.
This property holds for linear orders with order topology as well as their products.
@[protected, instance]
def
order_dual.Sup_convergence_class
{α : Type u_1}
[preorder α]
[topological_space α]
[Inf_convergence_class α] :
@[protected, instance]
def
order_dual.Inf_convergence_class
{α : Type u_1}
[preorder α]
[topological_space α]
[Sup_convergence_class α] :
@[protected, instance]
def
linear_order.Sup_convergence_class
{α : Type u_1}
[topological_space α]
[linear_order α]
[order_topology α] :
@[protected, instance]
def
linear_order.Inf_convergence_class
{α : Type u_1}
[topological_space α]
[linear_order α]
[order_topology α] :
theorem
tendsto_at_top_is_lub
{α : Type u_1}
{ι : Type u_3}
[preorder ι]
[topological_space α]
[preorder α]
[Sup_convergence_class α]
{f : ι → α}
{a : α}
(h_mono : monotone f)
(ha : is_lub (set.range f) a) :
filter.tendsto f filter.at_top (nhds a)
theorem
tendsto_at_bot_is_lub
{α : Type u_1}
{ι : Type u_3}
[preorder ι]
[topological_space α]
[preorder α]
[Sup_convergence_class α]
{f : ι → α}
{a : α}
(h_anti : antitone f)
(ha : is_lub (set.range f) a) :
filter.tendsto f filter.at_bot (nhds a)
theorem
tendsto_at_bot_is_glb
{α : Type u_1}
{ι : Type u_3}
[preorder ι]
[topological_space α]
[preorder α]
[Inf_convergence_class α]
{f : ι → α}
{a : α}
(h_mono : monotone f)
(ha : is_glb (set.range f) a) :
filter.tendsto f filter.at_bot (nhds a)
theorem
tendsto_at_top_is_glb
{α : Type u_1}
{ι : Type u_3}
[preorder ι]
[topological_space α]
[preorder α]
[Inf_convergence_class α]
{f : ι → α}
{a : α}
(h_anti : antitone f)
(ha : is_glb (set.range f) a) :
filter.tendsto f filter.at_top (nhds a)
theorem
tendsto_at_top_csupr
{α : Type u_1}
{ι : Type u_3}
[preorder ι]
[topological_space α]
[conditionally_complete_lattice α]
[Sup_convergence_class α]
{f : ι → α}
(h_mono : monotone f)
(hbdd : bdd_above (set.range f)) :
filter.tendsto f filter.at_top (nhds (⨆ (i : ι), f i))
theorem
tendsto_at_bot_csupr
{α : Type u_1}
{ι : Type u_3}
[preorder ι]
[topological_space α]
[conditionally_complete_lattice α]
[Sup_convergence_class α]
{f : ι → α}
(h_anti : antitone f)
(hbdd : bdd_above (set.range f)) :
filter.tendsto f filter.at_bot (nhds (⨆ (i : ι), f i))
theorem
tendsto_at_bot_cinfi
{α : Type u_1}
{ι : Type u_3}
[preorder ι]
[topological_space α]
[conditionally_complete_lattice α]
[Inf_convergence_class α]
{f : ι → α}
(h_mono : monotone f)
(hbdd : bdd_below (set.range f)) :
filter.tendsto f filter.at_bot (nhds (⨅ (i : ι), f i))
theorem
tendsto_at_top_cinfi
{α : Type u_1}
{ι : Type u_3}
[preorder ι]
[topological_space α]
[conditionally_complete_lattice α]
[Inf_convergence_class α]
{f : ι → α}
(h_anti : antitone f)
(hbdd : bdd_below (set.range f)) :
filter.tendsto f filter.at_top (nhds (⨅ (i : ι), f i))
theorem
tendsto_at_top_supr
{α : Type u_1}
{ι : Type u_3}
[preorder ι]
[topological_space α]
[complete_lattice α]
[Sup_convergence_class α]
{f : ι → α}
(h_mono : monotone f) :
filter.tendsto f filter.at_top (nhds (⨆ (i : ι), f i))
theorem
tendsto_at_bot_supr
{α : Type u_1}
{ι : Type u_3}
[preorder ι]
[topological_space α]
[complete_lattice α]
[Sup_convergence_class α]
{f : ι → α}
(h_anti : antitone f) :
filter.tendsto f filter.at_bot (nhds (⨆ (i : ι), f i))
theorem
tendsto_at_bot_infi
{α : Type u_1}
{ι : Type u_3}
[preorder ι]
[topological_space α]
[complete_lattice α]
[Inf_convergence_class α]
{f : ι → α}
(h_mono : monotone f) :
filter.tendsto f filter.at_bot (nhds (⨅ (i : ι), f i))
theorem
tendsto_at_top_infi
{α : Type u_1}
{ι : Type u_3}
[preorder ι]
[topological_space α]
[complete_lattice α]
[Inf_convergence_class α]
{f : ι → α}
(h_anti : antitone f) :
filter.tendsto f filter.at_top (nhds (⨅ (i : ι), f i))
@[protected, instance]
def
prod.Sup_convergence_class
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
[topological_space α]
[topological_space β]
[Sup_convergence_class α]
[Sup_convergence_class β] :
Sup_convergence_class (α × β)
@[protected, instance]
def
prod.Inf_convergence_class
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
[topological_space α]
[topological_space β]
[Inf_convergence_class α]
[Inf_convergence_class β] :
Inf_convergence_class (α × β)
@[protected, instance]
def
pi.Sup_convergence_class
{ι : Type u_1}
{α : ι → Type u_2}
[Π (i : ι), preorder (α i)]
[Π (i : ι), topological_space (α i)]
[∀ (i : ι), Sup_convergence_class (α i)] :
Sup_convergence_class (Π (i : ι), α i)
@[protected, instance]
def
pi.Inf_convergence_class
{ι : Type u_1}
{α : ι → Type u_2}
[Π (i : ι), preorder (α i)]
[Π (i : ι), topological_space (α i)]
[∀ (i : ι), Inf_convergence_class (α i)] :
Inf_convergence_class (Π (i : ι), α i)
@[protected, instance]
def
pi.Sup_convergence_class'
{α : Type u_1}
{ι : Type u_2}
[preorder α]
[topological_space α]
[Sup_convergence_class α] :
Sup_convergence_class (ι → α)
@[protected, instance]
def
pi.Inf_convergence_class'
{α : Type u_1}
{ι : Type u_2}
[preorder α]
[topological_space α]
[Inf_convergence_class α] :
Inf_convergence_class (ι → α)
theorem
tendsto_of_monotone
{ι : Type u_1}
{α : Type u_2}
[preorder ι]
[topological_space α]
[conditionally_complete_linear_order α]
[order_topology α]
{f : ι → α}
(h_mono : monotone f) :
filter.tendsto f filter.at_top filter.at_top ∨ ∃ (l : α), filter.tendsto f filter.at_top (nhds l)
theorem
tendsto_iff_tendsto_subseq_of_monotone
{ι₁ : Type u_1}
{ι₂ : Type u_2}
{α : Type u_3}
[semilattice_sup ι₁]
[preorder ι₂]
[nonempty ι₁]
[topological_space α]
[conditionally_complete_linear_order α]
[order_topology α]
[no_max_order α]
{f : ι₂ → α}
{φ : ι₁ → ι₂}
{l : α}
(hf : monotone f)
(hg : filter.tendsto φ filter.at_top filter.at_top) :
filter.tendsto f filter.at_top (nhds l) ↔ filter.tendsto (f ∘ φ) filter.at_top (nhds l)
The next family of results, such as is_lub_of_tendsto_at_top and supr_eq_of_tendsto, are
converses to the standard fact that bounded monotone functions converge. They state, that if a
monotone function f tends to a along filter.at_top, then that value a is a least upper bound
for the range of f.
Related theorems above (is_lub.is_lub_of_tendsto, is_glb.is_glb_of_tendsto etc) cover the case
when f x tends to a as x tends to some point b in the domain.
theorem
monotone.ge_of_tendsto
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[preorder α]
[order_closed_topology α]
[semilattice_sup β]
{f : β → α}
{a : α}
(hf : monotone f)
(ha : filter.tendsto f filter.at_top (nhds a))
(b : β) :
f b ≤ a
theorem
monotone.le_of_tendsto
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[preorder α]
[order_closed_topology α]
[semilattice_inf β]
{f : β → α}
{a : α}
(hf : monotone f)
(ha : filter.tendsto f filter.at_bot (nhds a))
(b : β) :
a ≤ f b
theorem
antitone.le_of_tendsto
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[preorder α]
[order_closed_topology α]
[semilattice_sup β]
{f : β → α}
{a : α}
(hf : antitone f)
(ha : filter.tendsto f filter.at_top (nhds a))
(b : β) :
a ≤ f b
theorem
antitone.ge_of_tendsto
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[preorder α]
[order_closed_topology α]
[semilattice_inf β]
{f : β → α}
{a : α}
(hf : antitone f)
(ha : filter.tendsto f filter.at_bot (nhds a))
(b : β) :
f b ≤ a
theorem
is_lub_of_tendsto_at_top
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[preorder α]
[order_closed_topology α]
[nonempty β]
[semilattice_sup β]
{f : β → α}
{a : α}
(hf : monotone f)
(ha : filter.tendsto f filter.at_top (nhds a)) :
theorem
is_glb_of_tendsto_at_bot
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[preorder α]
[order_closed_topology α]
[nonempty β]
[semilattice_inf β]
{f : β → α}
{a : α}
(hf : monotone f)
(ha : filter.tendsto f filter.at_bot (nhds a)) :
theorem
is_lub_of_tendsto_at_bot
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[preorder α]
[order_closed_topology α]
[nonempty β]
[semilattice_inf β]
{f : β → α}
{a : α}
(hf : antitone f)
(ha : filter.tendsto f filter.at_bot (nhds a)) :
theorem
is_glb_of_tendsto_at_top
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[preorder α]
[order_closed_topology α]
[nonempty β]
[semilattice_sup β]
{f : β → α}
{a : α}
(hf : antitone f)
(ha : filter.tendsto f filter.at_top (nhds a)) :
theorem
supr_eq_of_tendsto
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[complete_linear_order α]
[order_topology α]
[nonempty β]
[semilattice_sup β]
{f : β → α}
{a : α}
(hf : monotone f) :
filter.tendsto f filter.at_top (nhds a) → supr f = a
theorem
infi_eq_of_tendsto
{β : Type u_2}
{α : Type u_1}
[topological_space α]
[complete_linear_order α]
[order_topology α]
[nonempty β]
[semilattice_sup β]
{f : β → α}
{a : α}
(hf : antitone f) :
filter.tendsto f filter.at_top (nhds a) → infi f = a
theorem
supr_eq_supr_subseq_of_monotone
{ι₁ : Type u_1}
{ι₂ : Type u_2}
{α : Type u_3}
[preorder ι₂]
[complete_lattice α]
{l : filter ι₁}
[l.ne_bot]
{f : ι₂ → α}
{φ : ι₁ → ι₂}
(hf : monotone f)
(hφ : filter.tendsto φ l filter.at_top) :
theorem
infi_eq_infi_subseq_of_monotone
{ι₁ : Type u_1}
{ι₂ : Type u_2}
{α : Type u_3}
[preorder ι₂]
[complete_lattice α]
{l : filter ι₁}
[l.ne_bot]
{f : ι₂ → α}
{φ : ι₁ → ι₂}
(hf : monotone f)
(hφ : filter.tendsto φ l filter.at_bot) :