Documentation

Mathlib.Topology.Order.MonotoneConvergence

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 aFilter.Tendsto CoeTC.coe Filter.atTop (nhds a)

    proof that a monotone function tends to 𝓝 a as x → ∞

Instances
    theorem SupConvergenceClass.tendsto_coe_atTop_isLUB {α : Type u_3} [Preorder α] [TopologicalSpace α] [self : SupConvergenceClass α] (a : α) (s : Set α) :
    IsLUB s aFilter.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 aFilter.Tendsto CoeTC.coe Filter.atBot (nhds a)

      proof that a monotone function tends to 𝓝 a as x → -∞

    Instances
      theorem InfConvergenceClass.tendsto_coe_atBot_isGLB {α : Type u_3} [Preorder α] [TopologicalSpace α] [self : InfConvergenceClass α] (a : α) (s : Set α) :
      IsGLB s aFilter.Tendsto CoeTC.coe Filter.atBot (nhds a)

      proof that a monotone function tends to 𝓝 a as x → -∞

      @[instance 100]
      Equations
      • =
      @[instance 100]
      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 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 α] :
      Equations
      • =
      instance Pi.infConvergenceClass' {α : Type u_1} {ι : Type u_3} [Preorder α] [TopologicalSpace α] [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)