Bounded monotone sequences converge #
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 IsLUB.
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
We say that α is a SupConvergenceClass 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.atTop). We require this for ι = (s : Set α),
f = CoeTC.coe in the definition, then prove it for any f in tendsto_atTop_isLUB.
This property holds for linear orders with order topology as well as their products.
- tendsto_coe_atTop_isLUB : ∀ (a : α) (s : Set α), IsLUB s a → Filter.Tendsto CoeTC.coe Filter.atTop (nhds a)
proof that a monotone function tends to
𝓝 aasx → ∞
Instances
theorem
SupConvergenceClass.tendsto_coe_atTop_isLUB
{α : Type u_3}
[Preorder α]
[TopologicalSpace α]
[self : SupConvergenceClass α]
(a : α)
(s : Set α)
:
IsLUB s a → Filter.Tendsto CoeTC.coe Filter.atTop (nhds a)
proof that a monotone function tends to 𝓝 a as x → ∞
We say that α is an InfConvergenceClass 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.atBot). We require this for ι = (s : Set α),
f = CoeTC.coe in the definition, then prove it for any f in tendsto_atBot_isGLB.
This property holds for linear orders with order topology as well as their products.
- tendsto_coe_atBot_isGLB : ∀ (a : α) (s : Set α), IsGLB s a → Filter.Tendsto CoeTC.coe Filter.atBot (nhds a)
proof that a monotone function tends to
𝓝 aasx → -∞
Instances
theorem
InfConvergenceClass.tendsto_coe_atBot_isGLB
{α : Type u_3}
[Preorder α]
[TopologicalSpace α]
[self : InfConvergenceClass α]
(a : α)
(s : Set α)
:
IsGLB s a → Filter.Tendsto CoeTC.coe Filter.atBot (nhds a)
proof that a monotone function tends to 𝓝 a as x → -∞
instance
OrderDual.supConvergenceClass
{α : Type u_1}
[Preorder α]
[TopologicalSpace α]
[InfConvergenceClass α]
:
Equations
- ⋯ = ⋯
instance
OrderDual.infConvergenceClass
{α : Type u_1}
[Preorder α]
[TopologicalSpace α]
[SupConvergenceClass α]
:
Equations
- ⋯ = ⋯
@[instance 100]
instance
LinearOrder.supConvergenceClass
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
:
Equations
- ⋯ = ⋯
@[instance 100]
instance
LinearOrder.infConvergenceClass
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
:
Equations
- ⋯ = ⋯
theorem
tendsto_atTop_isLUB
{α : Type u_1}
{ι : Type u_3}
[Preorder ι]
[TopologicalSpace α]
[Preorder α]
[SupConvergenceClass α]
{f : ι → α}
{a : α}
(h_mono : Monotone f)
(ha : IsLUB (Set.range f) a)
:
Filter.Tendsto f Filter.atTop (nhds a)
theorem
tendsto_atBot_isLUB
{α : Type u_1}
{ι : Type u_3}
[Preorder ι]
[TopologicalSpace α]
[Preorder α]
[SupConvergenceClass α]
{f : ι → α}
{a : α}
(h_anti : Antitone f)
(ha : IsLUB (Set.range f) a)
:
Filter.Tendsto f Filter.atBot (nhds a)
theorem
tendsto_atBot_isGLB
{α : Type u_1}
{ι : Type u_3}
[Preorder ι]
[TopologicalSpace α]
[Preorder α]
[InfConvergenceClass α]
{f : ι → α}
{a : α}
(h_mono : Monotone f)
(ha : IsGLB (Set.range f) a)
:
Filter.Tendsto f Filter.atBot (nhds a)
theorem
tendsto_atTop_isGLB
{α : Type u_1}
{ι : Type u_3}
[Preorder ι]
[TopologicalSpace α]
[Preorder α]
[InfConvergenceClass α]
{f : ι → α}
{a : α}
(h_anti : Antitone f)
(ha : IsGLB (Set.range f) a)
:
Filter.Tendsto f Filter.atTop (nhds a)
theorem
tendsto_atTop_ciSup
{α : Type u_1}
{ι : Type u_3}
[Preorder ι]
[TopologicalSpace α]
[ConditionallyCompleteLattice α]
[SupConvergenceClass α]
{f : ι → α}
(h_mono : Monotone f)
(hbdd : BddAbove (Set.range f))
:
Filter.Tendsto f Filter.atTop (nhds (⨆ (i : ι), f i))
theorem
tendsto_atBot_ciSup
{α : Type u_1}
{ι : Type u_3}
[Preorder ι]
[TopologicalSpace α]
[ConditionallyCompleteLattice α]
[SupConvergenceClass α]
{f : ι → α}
(h_anti : Antitone f)
(hbdd : BddAbove (Set.range f))
:
Filter.Tendsto f Filter.atBot (nhds (⨆ (i : ι), f i))
theorem
tendsto_atBot_ciInf
{α : Type u_1}
{ι : Type u_3}
[Preorder ι]
[TopologicalSpace α]
[ConditionallyCompleteLattice α]
[InfConvergenceClass α]
{f : ι → α}
(h_mono : Monotone f)
(hbdd : BddBelow (Set.range f))
:
Filter.Tendsto f Filter.atBot (nhds (⨅ (i : ι), f i))
theorem
tendsto_atTop_ciInf
{α : Type u_1}
{ι : Type u_3}
[Preorder ι]
[TopologicalSpace α]
[ConditionallyCompleteLattice α]
[InfConvergenceClass α]
{f : ι → α}
(h_anti : Antitone f)
(hbdd : BddBelow (Set.range f))
:
Filter.Tendsto f Filter.atTop (nhds (⨅ (i : ι), f i))
theorem
tendsto_atTop_iSup
{α : Type u_1}
{ι : Type u_3}
[Preorder ι]
[TopologicalSpace α]
[CompleteLattice α]
[SupConvergenceClass α]
{f : ι → α}
(h_mono : Monotone f)
:
Filter.Tendsto f Filter.atTop (nhds (⨆ (i : ι), f i))
theorem
tendsto_atBot_iSup
{α : Type u_1}
{ι : Type u_3}
[Preorder ι]
[TopologicalSpace α]
[CompleteLattice α]
[SupConvergenceClass α]
{f : ι → α}
(h_anti : Antitone f)
:
Filter.Tendsto f Filter.atBot (nhds (⨆ (i : ι), f i))
theorem
tendsto_atBot_iInf
{α : Type u_1}
{ι : Type u_3}
[Preorder ι]
[TopologicalSpace α]
[CompleteLattice α]
[InfConvergenceClass α]
{f : ι → α}
(h_mono : Monotone f)
:
Filter.Tendsto f Filter.atBot (nhds (⨅ (i : ι), f i))
theorem
tendsto_atTop_iInf
{α : Type u_1}
{ι : Type u_3}
[Preorder ι]
[TopologicalSpace α]
[CompleteLattice α]
[InfConvergenceClass α]
{f : ι → α}
(h_anti : Antitone f)
:
Filter.Tendsto f Filter.atTop (nhds (⨅ (i : ι), f i))
instance
Prod.supConvergenceClass
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[TopologicalSpace α]
[TopologicalSpace β]
[SupConvergenceClass α]
[SupConvergenceClass β]
:
SupConvergenceClass (α × β)
Equations
- ⋯ = ⋯
instance
instInfConvergenceClassProd
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
[TopologicalSpace α]
[TopologicalSpace β]
[InfConvergenceClass α]
[InfConvergenceClass β]
:
InfConvergenceClass (α × β)
Equations
- ⋯ = ⋯
instance
Pi.supConvergenceClass
{ι : Type u_3}
{α : ι → Type u_4}
[(i : ι) → Preorder (α i)]
[(i : ι) → TopologicalSpace (α i)]
[∀ (i : ι), SupConvergenceClass (α i)]
:
SupConvergenceClass ((i : ι) → α i)
Equations
- ⋯ = ⋯
instance
Pi.infConvergenceClass
{ι : Type u_3}
{α : ι → Type u_4}
[(i : ι) → Preorder (α i)]
[(i : ι) → TopologicalSpace (α i)]
[∀ (i : ι), InfConvergenceClass (α i)]
:
InfConvergenceClass ((i : ι) → α i)
Equations
- ⋯ = ⋯
instance
Pi.supConvergenceClass'
{α : Type u_1}
{ι : Type u_3}
[Preorder α]
[TopologicalSpace α]
[SupConvergenceClass α]
:
SupConvergenceClass (ι → α)
Equations
- ⋯ = ⋯
instance
Pi.infConvergenceClass'
{α : Type u_1}
{ι : Type u_3}
[Preorder α]
[TopologicalSpace α]
[InfConvergenceClass α]
:
InfConvergenceClass (ι → α)
Equations
- ⋯ = ⋯
theorem
tendsto_of_monotone
{ι : Type u_3}
{α : Type u_4}
[Preorder ι]
[TopologicalSpace α]
[ConditionallyCompleteLinearOrder α]
[OrderTopology α]
{f : ι → α}
(h_mono : Monotone f)
:
Filter.Tendsto f Filter.atTop Filter.atTop ∨ ∃ (l : α), Filter.Tendsto f Filter.atTop (nhds l)
theorem
tendsto_of_antitone
{ι : Type u_3}
{α : Type u_4}
[Preorder ι]
[TopologicalSpace α]
[ConditionallyCompleteLinearOrder α]
[OrderTopology α]
{f : ι → α}
(h_mono : Antitone f)
:
Filter.Tendsto f Filter.atTop Filter.atBot ∨ ∃ (l : α), Filter.Tendsto f Filter.atTop (nhds l)
theorem
tendsto_iff_tendsto_subseq_of_monotone
{ι₁ : Type u_3}
{ι₂ : Type u_4}
{α : Type u_5}
[SemilatticeSup ι₁]
[Preorder ι₂]
[Nonempty ι₁]
[TopologicalSpace α]
[ConditionallyCompleteLinearOrder α]
[OrderTopology α]
[NoMaxOrder α]
{f : ι₂ → α}
{φ : ι₁ → ι₂}
{l : α}
(hf : Monotone f)
(hg : Filter.Tendsto φ Filter.atTop Filter.atTop)
:
Filter.Tendsto f Filter.atTop (nhds l) ↔ Filter.Tendsto (f ∘ φ) Filter.atTop (nhds l)
theorem
tendsto_iff_tendsto_subseq_of_antitone
{ι₁ : Type u_3}
{ι₂ : Type u_4}
{α : Type u_5}
[SemilatticeSup ι₁]
[Preorder ι₂]
[Nonempty ι₁]
[TopologicalSpace α]
[ConditionallyCompleteLinearOrder α]
[OrderTopology α]
[NoMinOrder α]
{f : ι₂ → α}
{φ : ι₁ → ι₂}
{l : α}
(hf : Antitone f)
(hg : Filter.Tendsto φ Filter.atTop Filter.atTop)
:
Filter.Tendsto f Filter.atTop (nhds l) ↔ Filter.Tendsto (f ∘ φ) Filter.atTop (nhds l)
The next family of results, such as isLUB_of_tendsto_atTop and iSup_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.atTop, then that value a is a least upper bound
for the range of f.
Related theorems above (IsLUB.isLUB_of_tendsto, IsGLB.isGLB_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}
[TopologicalSpace α]
[Preorder α]
[OrderClosedTopology α]
[SemilatticeSup β]
{f : β → α}
{a : α}
(hf : Monotone f)
(ha : Filter.Tendsto f Filter.atTop (nhds a))
(b : β)
:
f b ≤ a
theorem
Monotone.le_of_tendsto
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[Preorder α]
[OrderClosedTopology α]
[SemilatticeInf β]
{f : β → α}
{a : α}
(hf : Monotone f)
(ha : Filter.Tendsto f Filter.atBot (nhds a))
(b : β)
:
a ≤ f b
theorem
Antitone.le_of_tendsto
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[Preorder α]
[OrderClosedTopology α]
[SemilatticeSup β]
{f : β → α}
{a : α}
(hf : Antitone f)
(ha : Filter.Tendsto f Filter.atTop (nhds a))
(b : β)
:
a ≤ f b
theorem
Antitone.ge_of_tendsto
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[Preorder α]
[OrderClosedTopology α]
[SemilatticeInf β]
{f : β → α}
{a : α}
(hf : Antitone f)
(ha : Filter.Tendsto f Filter.atBot (nhds a))
(b : β)
:
f b ≤ a
theorem
isLUB_of_tendsto_atTop
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[Preorder α]
[OrderClosedTopology α]
[Nonempty β]
[SemilatticeSup β]
{f : β → α}
{a : α}
(hf : Monotone f)
(ha : Filter.Tendsto f Filter.atTop (nhds a))
:
theorem
isGLB_of_tendsto_atBot
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[Preorder α]
[OrderClosedTopology α]
[Nonempty β]
[SemilatticeInf β]
{f : β → α}
{a : α}
(hf : Monotone f)
(ha : Filter.Tendsto f Filter.atBot (nhds a))
:
theorem
isLUB_of_tendsto_atBot
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[Preorder α]
[OrderClosedTopology α]
[Nonempty β]
[SemilatticeInf β]
{f : β → α}
{a : α}
(hf : Antitone f)
(ha : Filter.Tendsto f Filter.atBot (nhds a))
:
theorem
isGLB_of_tendsto_atTop
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[Preorder α]
[OrderClosedTopology α]
[Nonempty β]
[SemilatticeSup β]
{f : β → α}
{a : α}
(hf : Antitone f)
(ha : Filter.Tendsto f Filter.atTop (nhds a))
:
theorem
iSup_eq_of_tendsto
{α : Type u_3}
{β : Type u_4}
[TopologicalSpace α]
[CompleteLinearOrder α]
[OrderTopology α]
[Nonempty β]
[SemilatticeSup β]
{f : β → α}
{a : α}
(hf : Monotone f)
:
Filter.Tendsto f Filter.atTop (nhds a) → iSup f = a
theorem
iInf_eq_of_tendsto
{β : Type u_2}
{α : Type u_3}
[TopologicalSpace α]
[CompleteLinearOrder α]
[OrderTopology α]
[Nonempty β]
[SemilatticeSup β]
{f : β → α}
{a : α}
(hf : Antitone f)
:
Filter.Tendsto f Filter.atTop (nhds a) → iInf f = a
theorem
iSup_eq_iSup_subseq_of_monotone
{ι₁ : Type u_3}
{ι₂ : Type u_4}
{α : Type u_5}
[Preorder ι₂]
[CompleteLattice α]
{l : Filter ι₁}
[l.NeBot]
{f : ι₂ → α}
{φ : ι₁ → ι₂}
(hf : Monotone f)
(hφ : Filter.Tendsto φ l Filter.atTop)
:
⨆ (i : ι₂), f i = ⨆ (i : ι₁), f (φ i)
theorem
iSup_eq_iSup_subseq_of_antitone
{ι₁ : Type u_3}
{ι₂ : Type u_4}
{α : Type u_5}
[Preorder ι₂]
[CompleteLattice α]
{l : Filter ι₁}
[l.NeBot]
{f : ι₂ → α}
{φ : ι₁ → ι₂}
(hf : Antitone f)
(hφ : Filter.Tendsto φ l Filter.atBot)
:
⨆ (i : ι₂), f i = ⨆ (i : ι₁), f (φ i)
theorem
iInf_eq_iInf_subseq_of_monotone
{ι₁ : Type u_3}
{ι₂ : Type u_4}
{α : Type u_5}
[Preorder ι₂]
[CompleteLattice α]
{l : Filter ι₁}
[l.NeBot]
{f : ι₂ → α}
{φ : ι₁ → ι₂}
(hf : Monotone f)
(hφ : Filter.Tendsto φ l Filter.atBot)
:
⨅ (i : ι₂), f i = ⨅ (i : ι₁), f (φ i)
theorem
iInf_eq_iInf_subseq_of_antitone
{ι₁ : Type u_3}
{ι₂ : Type u_4}
{α : Type u_5}
[Preorder ι₂]
[CompleteLattice α]
{l : Filter ι₁}
[l.NeBot]
{f : ι₂ → α}
{φ : ι₁ → ι₂}
(hf : Antitone f)
(hφ : Filter.Tendsto φ l Filter.atTop)
:
⨅ (i : ι₂), f i = ⨅ (i : ι₁), f (φ i)