mathlib3 documentation

topology.algebra.order.monotone_convergence

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]
structure Sup_convergence_class (α : Type u_3) [preorder α] [topological_space α] :
Prop

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.

Instances of this typeclass
@[class]
structure Inf_convergence_class (α : Type u_3) [preorder α] [topological_space α] :
Prop

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.

Instances of this typeclass
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) :
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) :
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) :
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) :
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)) :
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)) :
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)) :
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)) :
theorem tendsto_at_top_supr {α : Type u_1} {ι : Type u_3} [preorder ι] [topological_space α] [complete_lattice α] [Sup_convergence_class α] {f : ι α} (h_mono : monotone f) :
theorem tendsto_at_bot_supr {α : Type u_1} {ι : Type u_3} [preorder ι] [topological_space α] [complete_lattice α] [Sup_convergence_class α] {f : ι α} (h_anti : antitone f) :
theorem tendsto_at_bot_infi {α : Type u_1} {ι : Type u_3} [preorder ι] [topological_space α] [complete_lattice α] [Inf_convergence_class α] {f : ι α} (h_mono : monotone f) :
theorem tendsto_at_top_infi {α : Type u_1} {ι : Type u_3} [preorder ι] [topological_space α] [complete_lattice α] [Inf_convergence_class α] {f : ι α} (h_anti : antitone f) :
@[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]
@[protected, instance]
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) :

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) :
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) :
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) :
( (i : ι₂), f i) = (i : ι₁), f (φ i)
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) :
( (i : ι₂), f i) = (i : ι₁), f (φ i)