LeanEconTheory
Contraction Mapping

Imports

import Mathlib.Data.Real.Basic
import Mathlib.Tactic
import Mathlib.Topology.ContinuousMap.Bounded.Basic

Contraction Mapping

Introduction

This page lays out the Lean formalization code of the Contraction Mapping Theorem and Blackwell's Sufficiency Theorem for bounded continuous functions. A graphical visualization of the relevant mathematical dependencies can be viewed here.

Setup

Tell Lean to interpret any use of X to be of Nonempty, TopologicalSpace type. The curly braces denote the implicit argument and type inferred by Lean.

variable {X : Type*} [Nonempty X] [TopologicalSpace X]

First, we define a structure for a contraction mapping from the space of bounded continuous functions to the space of bounded continuous functions.

Definition: Contraction Mapping

Let B(X) be the space of bounded continuous functions, (B(X), d) be a metric space (d being the sup-norm), and T : B(X) \rightarrow B(X) be a function mapping B(X) to itself. The function T is a contraction mapping if there exists a number \beta \in (0, 1) satisfying d(Tf, Tg) \leq \beta d(f, g)\text{ for all }f, g \in B(X).

open BoundedContinuousFunction

structure IsContraction (T : BoundedContinuousFunction X ℝ → BoundedContinuousFunction X ℝ) where
  β : ℝ
  hβ_gt0 : 0 < β
  hβ_lt1 : β < 1
  h_dist : ∀ (f g : X →ᵇ ℝ), dist (T f) (T g) ≤ β * dist f g

To prove certain properties of a contraction mapping, it will be helpful to know that contraction mappings are continuous.

Lemma: Contraction Mappings are Continuous

For all f_0 ∈ B(X) and ε > 0 there exists a δ such that whenever f ∈ B(X) such that d(f, f_0) < δ, we have d(Tf, Tf_0) < ε.

Proof.
Fix an arbitrary f_0 ∈ B(X) and ε > 0 and pick δ = ε. Then d(Tf, Tf_0) ≤ β d(f, f_0) ≤ β δ = β ε < ε. ■

omit [Nonempty X] in
lemma IsContractionIsContinuous {T : BoundedContinuousFunction X ℝ → BoundedContinuousFunction X ℝ} (hT : IsContraction T) : Continuous T := byX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝhT:IsContraction T⊢ Continuous T
  -- Extract β and its properties from the contraction definition
  rcases hT with ⟨β, hβ0, hβ1, h_dist⟩X:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝβ:ℝhβ0:0 < βhβ1:β < 1h_dist:∀ (f g : X →ᵇ ℝ), dist (T f) (T g) ≤ β * dist f g⊢ Continuous T
  -- Use the metric space ε-δ definition of continuity
  rw [Metric.continuous_iff]X:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝβ:ℝhβ0:0 < βhβ1:β < 1h_dist:∀ (f g : X →ᵇ ℝ), dist (T f) (T g) ≤ β * dist f g⊢ ∀ (b : X →ᵇ ℝ), ∀ ε > 0, ∃ δ > 0, ∀ (a : X →ᵇ ℝ), dist a b < δ → dist (T a) (T b) < ε
  intro f₀ εX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝβ:ℝhβ0:0 < βhβ1:β < 1h_dist:∀ (f g : X →ᵇ ℝ), dist (T f) (T g) ≤ β * dist f gf₀:X →ᵇ ℝε:ℝ⊢ ε > 0 → ∃ δ > 0, ∀ (a : X →ᵇ ℝ), dist a f₀ < δ → dist (T a) (T f₀) < ε hεX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝβ:ℝhβ0:0 < βhβ1:β < 1h_dist:∀ (f g : X →ᵇ ℝ), dist (T f) (T g) ≤ β * dist f gf₀:X →ᵇ ℝε:ℝhε:ε > 0⊢ ∃ δ > 0, ∀ (a : X →ᵇ ℝ), dist a f₀ < δ → dist (T a) (T f₀) < ε
  -- Choose δ = ε (implicitly with ε > 0)
  use ε, hεrightX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝβ:ℝhβ0:0 < βhβ1:β < 1h_dist:∀ (f g : X →ᵇ ℝ), dist (T f) (T g) ≤ β * dist f gf₀:X →ᵇ ℝε:ℝhε:ε > 0⊢ ∀ (a : X →ᵇ ℝ), dist a f₀ < ε → dist (T a) (T f₀) < ε
  intro f hsrightX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝβ:ℝhβ0:0 < βhβ1:β < 1h_dist:∀ (f g : X →ᵇ ℝ), dist (T f) (T g) ≤ β * dist f gf₀:X →ᵇ ℝε:ℝhε:ε > 0f:X →ᵇ ℝhs:dist f f₀ < ε⊢ dist (T f) (T f₀) < ε
  -- We know dist (T f) (T f₀) ≤ β * dist f f₀ by the definition of a contraction mapping
  have h_le := h_dist f f₀rightX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝβ:ℝhβ0:0 < βhβ1:β < 1h_dist:∀ (f g : X →ᵇ ℝ), dist (T f) (T g) ≤ β * dist f gf₀:X →ᵇ ℝε:ℝhε:ε > 0f:X →ᵇ ℝhs:dist f f₀ < εh_le:dist (T f) (T f₀) ≤ β * dist f f₀⊢ dist (T f) (T f₀) < ε
  -- Since dist f f₀ < ε and β > 0, we have β * dist f f₀ < β * ε
  have h1 : β * dist f f₀ < β * ε := mul_lt_mul_of_pos_left hs hβ0rightX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝβ:ℝhβ0:0 < βhβ1:β < 1h_dist:∀ (f g : X →ᵇ ℝ), dist (T f) (T g) ≤ β * dist f gf₀:X →ᵇ ℝε:ℝhε:ε > 0f:X →ᵇ ℝhs:dist f f₀ < εh_le:dist (T f) (T f₀) ≤ β * dist f f₀h1:β * dist f f₀ < β * ε⊢ dist (T f) (T f₀) < ε
  -- Since β < 1 and 0 < ε, we have β * ε < 1 * ε
  have h2 : β * ε < 1 * ε := mul_lt_mul_of_pos_right hβ1 hεrightX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝβ:ℝhβ0:0 < βhβ1:β < 1h_dist:∀ (f g : X →ᵇ ℝ), dist (T f) (T g) ≤ β * dist f gf₀:X →ᵇ ℝε:ℝhε:ε > 0f:X →ᵇ ℝhs:dist f f₀ < εh_le:dist (T f) (T f₀) ≤ β * dist f f₀h1:β * dist f f₀ < β * εh2:β * ε < 1 * ε⊢ dist (T f) (T f₀) < ε
  rw [one_mul] at h2rightX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝβ:ℝhβ0:0 < βhβ1:β < 1h_dist:∀ (f g : X →ᵇ ℝ), dist (T f) (T g) ≤ β * dist f gf₀:X →ᵇ ℝε:ℝhε:ε > 0f:X →ᵇ ℝhs:dist f f₀ < εh_le:dist (T f) (T f₀) ≤ β * dist f f₀h1:β * dist f f₀ < β * εh2:β * ε < ε⊢ dist (T f) (T f₀) < ε
  -- Combine the above two remarks to get β * dist f f₀ < ε
  have h_lt : β * dist f f₀ < ε := lt_trans h1 h2rightX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝβ:ℝhβ0:0 < βhβ1:β < 1h_dist:∀ (f g : X →ᵇ ℝ), dist (T f) (T g) ≤ β * dist f gf₀:X →ᵇ ℝε:ℝhε:ε > 0f:X →ᵇ ℝhs:dist f f₀ < εh_le:dist (T f) (T f₀) ≤ β * dist f f₀h1:β * dist f f₀ < β * εh2:β * ε < εh_lt:β * dist f f₀ < ε⊢ dist (T f) (T f₀) < ε
  -- Conclude that dist (T f) (T f₀) < ε
  exact lt_of_le_of_lt h_le h_ltAll goals completed! 🐙

Now, we define a fixed point of the operator.

Definition: Fixed Point

def IsFixedPoint (v : BoundedContinuousFunction X ℝ) (T : BoundedContinuousFunction X ℝ → BoundedContinuousFunction X ℝ) : Prop :=
  T v = v

A final result to help us prove the Contraction Mapping Theorem is a bound on the difference of a sequence defined by the repeated application of the contraction map to an element in our metric space.

Lemma: Bound Difference One

d(T^n v_0, T^{n + 1} v_0) ≤ β^n d(v_0, T v_0) Proof.
We can use induction to prove this result. We can verify that for the base case of n = 1 we have that d(T v_0, T^2 v_0) ≤ β d(v_0, T v_0) using the contraction property of the map. The induction hypothesis is that d(T^k v_0, T^{k + 1} v_0) ≤ β^k d(v_0, T v_0). We verify the induction step by applying the contraction property of the map before invoking the induction hypothesis: d(T^{k + 1} v_0, T^{k + 2} v_0) ≤ β d(T^k v_0, T^{k + 1} v_0) ≤ β β^k d(v_0, T v_0) ≤ β^{k + 1} d(v_0, T v_0). ■

omit [Nonempty X] in
lemma bound_difference_one {T : BoundedContinuousFunction X ℝ → BoundedContinuousFunction X ℝ} (v₀ : BoundedContinuousFunction X ℝ) (hT : IsContraction T): ∀ n : ℕ, dist (T^[n] v₀) (T^[n + 1] v₀) ≤ hT.β^n * dist v₀ (T v₀) := byX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝv₀:X →ᵇ ℝhT:IsContraction T⊢ ∀ (n : ℕ), dist (T^[n] v₀) (T^[n + 1] v₀) ≤ hT.β ^ n * dist v₀ (T v₀)
  obtain ⟨β, hβ_gt0, hβ_lt1, h_dist⟩ := hTX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝv₀:X →ᵇ ℝβ:ℝhβ_gt0:0 < βhβ_lt1:β < 1h_dist:∀ (f g : X →ᵇ ℝ), dist (T f) (T g) ≤ β * dist f g⊢ ∀ (n : ℕ),
  dist (T^[n] v₀) (T^[n + 1] v₀) ≤
    { β := β, hβ_gt0 := hβ_gt0, hβ_lt1 := hβ_lt1, h_dist := h_dist }.β ^ n * dist v₀ (T v₀)
  -- Extract weak inequalities for β from strict inequalities
  have hβ_ge0 : 0 ≤ β := le_of_lt hβ_gt0X:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝv₀:X →ᵇ ℝβ:ℝhβ_gt0:0 < βhβ_lt1:β < 1h_dist:∀ (f g : X →ᵇ ℝ), dist (T f) (T g) ≤ β * dist f ghβ_ge0:0 ≤ β⊢ ∀ (n : ℕ),
  dist (T^[n] v₀) (T^[n + 1] v₀) ≤
    { β := β, hβ_gt0 := hβ_gt0, hβ_lt1 := hβ_lt1, h_dist := h_dist }.β ^ n * dist v₀ (T v₀)
  intro nX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝv₀:X →ᵇ ℝβ:ℝhβ_gt0:0 < βhβ_lt1:β < 1h_dist:∀ (f g : X →ᵇ ℝ), dist (T f) (T g) ≤ β * dist f ghβ_ge0:0 ≤ βn:ℕ⊢ dist (T^[n] v₀) (T^[n + 1] v₀) ≤ { β := β, hβ_gt0 := hβ_gt0, hβ_lt1 := hβ_lt1, h_dist := h_dist }.β ^ n * dist v₀ (T v₀)
  induction n with
  | zero =>zeroX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝv₀:X →ᵇ ℝβ:ℝhβ_gt0:0 < βhβ_lt1:β < 1h_dist:∀ (f g : X →ᵇ ℝ), dist (T f) (T g) ≤ β * dist f ghβ_ge0:0 ≤ β⊢ dist (T^[0] v₀) (T^[0 + 1] v₀) ≤ { β := β, hβ_gt0 := hβ_gt0, hβ_lt1 := hβ_lt1, h_dist := h_dist }.β ^ 0 * dist v₀ (T v₀)
    rw [pow_zero, one_mul]zeroX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝv₀:X →ᵇ ℝβ:ℝhβ_gt0:0 < βhβ_lt1:β < 1h_dist:∀ (f g : X →ᵇ ℝ), dist (T f) (T g) ≤ β * dist f ghβ_ge0:0 ≤ β⊢ dist (T^[0] v₀) (T^[0 + 1] v₀) ≤ dist v₀ (T v₀)
    rflAll goals completed! 🐙
  | succ k ih =>succX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝv₀:X →ᵇ ℝβ:ℝhβ_gt0:0 < βhβ_lt1:β < 1h_dist:∀ (f g : X →ᵇ ℝ), dist (T f) (T g) ≤ β * dist f ghβ_ge0:0 ≤ βk:ℕih:dist (T^[k] v₀) (T^[k + 1] v₀) ≤ { β := β, hβ_gt0 := hβ_gt0, hβ_lt1 := hβ_lt1, h_dist := h_dist }.β ^ k * dist v₀ (T v₀)⊢ dist (T^[k + 1] v₀) (T^[k + 1 + 1] v₀) ≤
  { β := β, hβ_gt0 := hβ_gt0, hβ_lt1 := hβ_lt1, h_dist := h_dist }.β ^ (k + 1) * dist v₀ (T v₀)
    -- Use `calc` to implement the transitive reasoning from the proof
    calc
      dist (T^[k + 1] v₀) (T^[k + 2] v₀)
      _ = dist (T (T^[k] v₀)) (T (T^[k + 1] v₀)) := byX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝv₀:X →ᵇ ℝβ:ℝhβ_gt0:0 < βhβ_lt1:β < 1h_dist:∀ (f g : X →ᵇ ℝ), dist (T f) (T g) ≤ β * dist f ghβ_ge0:0 ≤ βk:ℕih:dist (T^[k] v₀) (T^[k + 1] v₀) ≤ { β := β, hβ_gt0 := hβ_gt0, hβ_lt1 := hβ_lt1, h_dist := h_dist }.β ^ k * dist v₀ (T v₀)⊢ dist (T^[k + 1] v₀) (T^[k + 2] v₀) = dist (T (T^[k] v₀)) (T (T^[k + 1] v₀)) simp_rw [X:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝv₀:X →ᵇ ℝβ:ℝhβ_gt0:0 < βhβ_lt1:β < 1h_dist:∀ (f g : X →ᵇ ℝ), dist (T f) (T g) ≤ β * dist f ghβ_ge0:0 ≤ βk:ℕih:dist (T^[k] v₀) (T^[k + 1] v₀) ≤ { β := β, hβ_gt0 := hβ_gt0, hβ_lt1 := hβ_lt1, h_dist := h_dist }.β ^ k * dist v₀ (T v₀)⊢ dist (T^[k + 1] v₀) (T^[k + 2] v₀) = dist (T (T^[k] v₀)) (T (T^[k + 1] v₀))Function.iterate_succ_apply']
      _ ≤ β * dist (T^[k] v₀) (T^[k + 1] v₀) :=
        h_dist _ _
      _ ≤ β * (β^k * dist v₀ (T v₀)) :=
          mul_le_mul_of_nonneg_left ih hβ_ge0
      _ = β^(k+1) * dist v₀ (T v₀) := byX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝv₀:X →ᵇ ℝβ:ℝhβ_gt0:0 < βhβ_lt1:β < 1h_dist:∀ (f g : X →ᵇ ℝ), dist (T f) (T g) ≤ β * dist f ghβ_ge0:0 ≤ βk:ℕih:dist (T^[k] v₀) (T^[k + 1] v₀) ≤ { β := β, hβ_gt0 := hβ_gt0, hβ_lt1 := hβ_lt1, h_dist := h_dist }.β ^ k * dist v₀ (T v₀)⊢ β * (β ^ k * dist v₀ (T v₀)) = β ^ (k + 1) * dist v₀ (T v₀)
          ringAll goals completed! 🐙

Now, we are ready to prove the Contraction Mapping Theorem.

Theorem: Contraction Mapping Theorem

Let B(X) be a space of bounded continuous functions, (B(X), d) be a complete metric space and suppose that T : B(X) → B(X) is a contraction mapping with modulus β. Then we have the following two properties.

The operator T has exactly one fixed point v^* ∈ B(X).
For any v_0 ∈ B(X), and any $n ∈ ℕ$, we have d(T^n v_0, v^*) ≤ β^n d(v_0, v^*).

Proof.
Take some v_0 \in B(X).

I'll first prove existence of a fixed point. By Lemma: Bound Difference One, we know that d(T^n v_0, T^{n + 1} v_0) ≤ β^n d(v_0, T v_0), which converges to zero. By this geometric bound, the sequence \{T^n v_0\}_{n = 0}^∞ is a Cauchy sequence. By continuity of T, we also know that T v^* := T \lim_{n = 0}^∞ d(T^n v_0, T^{n + 1} v_0) = \lim_{n = 0}^∞ d(T^{n + 1} v_0, T^{n + 2} v_0) = v^*, meaning v^* is a fixed point.

I'll now prove uniqueness of the fixed point. If there exists another fixed point v', we must have d(v^*, v') =: a > 0. We then reach a contradiction with 0 < a = d(v^*, v') = d(T v^*, T v') ≤ β d(v^*, v') = β a.
We can use induction to prove this second statement. For the base case of n = 0, we trivially have that d(v_0, v^*) ≤ d(v_0, v^*). We can prove the induction step by using the definition of the fixed point and the contraction property of the operator, before invoking the induction hypothesis. d(T^{k + 1} v_0, v^*) = d(T T^k v_0, T v^*) ≤ β d(T^k, v^*) = β · β^k d(v_0, v^*) = β^{k + 1} d(v_0, v^*)

■

omit [Nonempty X] in
theorem ContractionMappingTheorem {T : BoundedContinuousFunction X ℝ → BoundedContinuousFunction X ℝ} (hT : IsContraction T) :
  (∃! v_star : BoundedContinuousFunction X ℝ, IsFixedPoint v_star T) ∧
  (∀ v_star : BoundedContinuousFunction X ℝ, IsFixedPoint v_star T →
    ∀ (v₀ : BoundedContinuousFunction X ℝ) (n : ℕ), dist v_star (T^[n] v₀) ≤ hT.β^n * dist v_star v₀) := byX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝhT:IsContraction T⊢ (∃! v_star, IsFixedPoint v_star T) ∧
  ∀ (v_star : X →ᵇ ℝ),
    IsFixedPoint v_star T → ∀ (v₀ : X →ᵇ ℝ) (n : ℕ), dist v_star (T^[n] v₀) ≤ hT.β ^ n * dist v_star v₀
  -- Take $`v_0` by non-emptiness of $`B(X)`
  obtain ⟨v₀⟩ := (inferInstance : Nonempty (BoundedContinuousFunction X ℝ))X:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝhT:IsContraction Tv₀:X →ᵇ ℝ⊢ (∃! v_star, IsFixedPoint v_star T) ∧
  ∀ (v_star : X →ᵇ ℝ),
    IsFixedPoint v_star T → ∀ (v₀ : X →ᵇ ℝ) (n : ℕ), dist v_star (T^[n] v₀) ≤ hT.β ^ n * dist v_star v₀
  -- Add a weak inequality for β from the strict inequality
  have hβ_ge0 : 0 ≤ hT.β := le_of_lt hT.hβ_gt0X:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝhT:IsContraction Tv₀:X →ᵇ ℝhβ_ge0:0 ≤ hT.β⊢ (∃! v_star, IsFixedPoint v_star T) ∧
  ∀ (v_star : X →ᵇ ℝ),
    IsFixedPoint v_star T → ∀ (v₀ : X →ᵇ ℝ) (n : ℕ), dist v_star (T^[n] v₀) ≤ hT.β ^ n * dist v_star v₀
  -- Prove the sequence is Cauchy using our geometric bound
  have h_cauchy : CauchySeq (fun n => T^[n] v₀) := byX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝhT:IsContraction T⊢ (∃! v_star, IsFixedPoint v_star T) ∧
  ∀ (v_star : X →ᵇ ℝ),
    IsFixedPoint v_star T → ∀ (v₀ : X →ᵇ ℝ) (n : ℕ), dist v_star (T^[n] v₀) ≤ hT.β ^ n * dist v_star v₀
    -- Mathlib provides a tool to deduce Cauchy sequences directly from geometric bounds
    apply cauchySeq_of_le_geometric hT.β (dist v₀ (T v₀)) hT.hβ_lt1X:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝhT:IsContraction Tv₀:X →ᵇ ℝhβ_ge0:0 ≤ hT.β⊢ ∀ (n : ℕ), dist (T^[n] v₀) (T^[n + 1] v₀) ≤ dist v₀ (T v₀) * hT.β ^ n
    intro nX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝhT:IsContraction Tv₀:X →ᵇ ℝhβ_ge0:0 ≤ hT.βn:ℕ⊢ dist (T^[n] v₀) (T^[n + 1] v₀) ≤ dist v₀ (T v₀) * hT.β ^ n
    calc
      dist (T^[n] v₀) (T^[n + 1] v₀)
      _ ≤ hT.β^n * dist v₀ (T v₀) := bound_difference_one v₀ hT n
      _ = dist v₀ (T v₀) * hT.β^n := mul_comm _ _
  -- Get v_star from the Cauchy sequence convergence
  have h_converges : ∃ x, Filter.Tendsto (fun n => T^[n] v₀) Filter.atTop (nhds x) :=  -- `atTop` means for infinite values
    cauchySeq_tendsto_of_complete h_cauchyX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝhT:IsContraction Tv₀:X →ᵇ ℝhβ_ge0:0 ≤ hT.βh_cauchy:CauchySeq fun n ↦ T^[n] v₀h_converges:∃ x, Filter.Tendsto (fun n ↦ T^[n] v₀) Filter.atTop (nhds x)⊢ (∃! v_star, IsFixedPoint v_star T) ∧
  ∀ (v_star : X →ᵇ ℝ),
    IsFixedPoint v_star T → ∀ (v₀ : X →ᵇ ℝ) (n : ℕ), dist v_star (T^[n] v₀) ≤ hT.β ^ n * dist v_star v₀
  obtain ⟨v_star, h_lim⟩ := h_convergesX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝhT:IsContraction Tv₀:X →ᵇ ℝhβ_ge0:0 ≤ hT.βh_cauchy:CauchySeq fun n ↦ T^[n] v₀v_star:X →ᵇ ℝh_lim:Filter.Tendsto (fun n ↦ T^[n] v₀) Filter.atTop (nhds v_star)⊢ (∃! v_star, IsFixedPoint v_star T) ∧
  ∀ (v_star : X →ᵇ ℝ),
    IsFixedPoint v_star T → ∀ (v₀ : X →ᵇ ℝ) (n : ℕ), dist v_star (T^[n] v₀) ≤ hT.β ^ n * dist v_star v₀
  -- Establish that v_star is a fixed point of T (T v_star = v_star)
  have h_fixed : IsFixedPoint v_star T := byX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝhT:IsContraction T⊢ (∃! v_star, IsFixedPoint v_star T) ∧
  ∀ (v_star : X →ᵇ ℝ),
    IsFixedPoint v_star T → ∀ (v₀ : X →ᵇ ℝ) (n : ℕ), dist v_star (T^[n] v₀) ≤ hT.β ^ n * dist v_star v₀
    change T v_star = v_starX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝhT:IsContraction Tv₀:X →ᵇ ℝhβ_ge0:0 ≤ hT.βh_cauchy:CauchySeq fun n ↦ T^[n] v₀v_star:X →ᵇ ℝh_lim:Filter.Tendsto (fun n ↦ T^[n] v₀) Filter.atTop (nhds v_star)⊢ T v_star = v_star  -- Change the goal to the definition of a fixed point
    -- We show T v_star = v_star by showing that both sides are limits of T^[n + 1] v₀
    have h1 : Filter.Tendsto (fun n => T^[n + 1] v₀) Filter.atTop (nhds (T v_star)) := byX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝhT:IsContraction T⊢ (∃! v_star, IsFixedPoint v_star T) ∧
  ∀ (v_star : X →ᵇ ℝ),
    IsFixedPoint v_star T → ∀ (v₀ : X →ᵇ ℝ) (n : ℕ), dist v_star (T^[n] v₀) ≤ hT.β ^ n * dist v_star v₀
      have h_cont : Continuous T := IsContractionIsContinuous hTX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝhT:IsContraction Tv₀:X →ᵇ ℝhβ_ge0:0 ≤ hT.βh_cauchy:CauchySeq fun n ↦ T^[n] v₀v_star:X →ᵇ ℝh_lim:Filter.Tendsto (fun n ↦ T^[n] v₀) Filter.atTop (nhds v_star)h_cont:Continuous T⊢ Filter.Tendsto (fun n ↦ T^[n + 1] v₀) Filter.atTop (nhds (T v_star))
      have h_tendsto := h_cont.tendsto v_starX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝhT:IsContraction Tv₀:X →ᵇ ℝhβ_ge0:0 ≤ hT.βh_cauchy:CauchySeq fun n ↦ T^[n] v₀v_star:X →ᵇ ℝh_lim:Filter.Tendsto (fun n ↦ T^[n] v₀) Filter.atTop (nhds v_star)h_cont:Continuous Th_tendsto:Filter.Tendsto T (nhds v_star) (nhds (T v_star))⊢ Filter.Tendsto (fun n ↦ T^[n + 1] v₀) Filter.atTop (nhds (T v_star))  -- Define a convergence neighborhood of the function
      simp_rw [X:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝhT:IsContraction Tv₀:X →ᵇ ℝhβ_ge0:0 ≤ hT.βh_cauchy:CauchySeq fun n ↦ T^[n] v₀v_star:X →ᵇ ℝh_lim:Filter.Tendsto (fun n ↦ T^[n] v₀) Filter.atTop (nhds v_star)h_cont:Continuous Th_tendsto:Filter.Tendsto T (nhds v_star) (nhds (T v_star))⊢ Filter.Tendsto (fun n ↦ T^[n + 1] v₀) Filter.atTop (nhds (T v_star))Function.iterate_succ_apply']
      exact Filter.Tendsto.comp h_tendsto h_limAll goals completed! 🐙  -- Chains continuity of T at v_star with the limit of the sequence to get the operator aplied to the converging sequence
    have h2 : Filter.Tendsto (fun n => T^[n + 1] v₀) Filter.atTop (nhds v_star) := byX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝhT:IsContraction T⊢ (∃! v_star, IsFixedPoint v_star T) ∧
  ∀ (v_star : X →ᵇ ℝ),
    IsFixedPoint v_star T → ∀ (v₀ : X →ᵇ ℝ) (n : ℕ), dist v_star (T^[n] v₀) ≤ hT.β ^ n * dist v_star v₀
      exact (Filter.tendsto_add_atTop_iff_nat 1).mpr h_limAll goals completed! 🐙  -- Apply the lemma backwards ("if")
    exact tendsto_nhds_unique h1 h2All goals completed! 🐙
  -- Combine the parts to solve the main conjunction goal
  constructorleftX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝhT:IsContraction Tv₀:X →ᵇ ℝhβ_ge0:0 ≤ hT.βh_cauchy:CauchySeq fun n ↦ T^[n] v₀v_star:X →ᵇ ℝh_lim:Filter.Tendsto (fun n ↦ T^[n] v₀) Filter.atTop (nhds v_star)h_fixed:IsFixedPoint v_star T⊢ ∃! v_star, IsFixedPoint v_star TrightX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝhT:IsContraction Tv₀:X →ᵇ ℝhβ_ge0:0 ≤ hT.βh_cauchy:CauchySeq fun n ↦ T^[n] v₀v_star:X →ᵇ ℝh_lim:Filter.Tendsto (fun n ↦ T^[n] v₀) Filter.atTop (nhds v_star)h_fixed:IsFixedPoint v_star T⊢ ∀ (v_star : X →ᵇ ℝ), IsFixedPoint v_star T → ∀ (v₀ : X →ᵇ ℝ) (n : ℕ), dist v_star (T^[n] v₀) ≤ hT.β ^ n * dist v_star v₀  -- Split up parts (a) and (b)
  -- (a)
  use v_starhX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝhT:IsContraction Tv₀:X →ᵇ ℝhβ_ge0:0 ≤ hT.βh_cauchy:CauchySeq fun n ↦ T^[n] v₀v_star:X →ᵇ ℝh_lim:Filter.Tendsto (fun n ↦ T^[n] v₀) Filter.atTop (nhds v_star)h_fixed:IsFixedPoint v_star T⊢ (fun v_star ↦ IsFixedPoint v_star T) v_star ∧ ∀ (y : X →ᵇ ℝ), (fun v_star ↦ IsFixedPoint v_star T) y → y = v_starrightX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝhT:IsContraction Tv₀:X →ᵇ ℝhβ_ge0:0 ≤ hT.βh_cauchy:CauchySeq fun n ↦ T^[n] v₀v_star:X →ᵇ ℝh_lim:Filter.Tendsto (fun n ↦ T^[n] v₀) Filter.atTop (nhds v_star)h_fixed:IsFixedPoint v_star T⊢ ∀ (v_star : X →ᵇ ℝ), IsFixedPoint v_star T → ∀ (v₀ : X →ᵇ ℝ) (n : ℕ), dist v_star (T^[n] v₀) ≤ hT.β ^ n * dist v_star v₀  -- Give v_star as the witness (candidate for unique existence)
  constructorh.leftX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝhT:IsContraction Tv₀:X →ᵇ ℝhβ_ge0:0 ≤ hT.βh_cauchy:CauchySeq fun n ↦ T^[n] v₀v_star:X →ᵇ ℝh_lim:Filter.Tendsto (fun n ↦ T^[n] v₀) Filter.atTop (nhds v_star)h_fixed:IsFixedPoint v_star T⊢ (fun v_star ↦ IsFixedPoint v_star T) v_starh.rightX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝhT:IsContraction Tv₀:X →ᵇ ℝhβ_ge0:0 ≤ hT.βh_cauchy:CauchySeq fun n ↦ T^[n] v₀v_star:X →ᵇ ℝh_lim:Filter.Tendsto (fun n ↦ T^[n] v₀) Filter.atTop (nhds v_star)h_fixed:IsFixedPoint v_star T⊢ ∀ (y : X →ᵇ ℝ), (fun v_star ↦ IsFixedPoint v_star T) y → y = v_starrightX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝhT:IsContraction Tv₀:X →ᵇ ℝhβ_ge0:0 ≤ hT.βh_cauchy:CauchySeq fun n ↦ T^[n] v₀v_star:X →ᵇ ℝh_lim:Filter.Tendsto (fun n ↦ T^[n] v₀) Filter.atTop (nhds v_star)h_fixed:IsFixedPoint v_star T⊢ ∀ (v_star : X →ᵇ ℝ), IsFixedPoint v_star T → ∀ (v₀ : X →ᵇ ℝ) (n : ℕ), dist v_star (T^[n] v₀) ≤ hT.β ^ n * dist v_star v₀  -- Split up the unique existence goal
  -- (i)  Prove that there exists a fixed point
  exact h_fixedh.rightX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝhT:IsContraction Tv₀:X →ᵇ ℝhβ_ge0:0 ≤ hT.βh_cauchy:CauchySeq fun n ↦ T^[n] v₀v_star:X →ᵇ ℝh_lim:Filter.Tendsto (fun n ↦ T^[n] v₀) Filter.atTop (nhds v_star)h_fixed:IsFixedPoint v_star T⊢ ∀ (y : X →ᵇ ℝ), (fun v_star ↦ IsFixedPoint v_star T) y → y = v_starrightX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝhT:IsContraction Tv₀:X →ᵇ ℝhβ_ge0:0 ≤ hT.βh_cauchy:CauchySeq fun n ↦ T^[n] v₀v_star:X →ᵇ ℝh_lim:Filter.Tendsto (fun n ↦ T^[n] v₀) Filter.atTop (nhds v_star)h_fixed:IsFixedPoint v_star T⊢ ∀ (v_star : X →ᵇ ℝ), IsFixedPoint v_star T → ∀ (v₀ : X →ᵇ ℝ) (n : ℕ), dist v_star (T^[n] v₀) ≤ hT.β ^ n * dist v_star v₀
  -- (ii) Prove that there exists a fixed point
  intro v_other hv_otherh.rightX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝhT:IsContraction Tv₀:X →ᵇ ℝhβ_ge0:0 ≤ hT.βh_cauchy:CauchySeq fun n ↦ T^[n] v₀v_star:X →ᵇ ℝh_lim:Filter.Tendsto (fun n ↦ T^[n] v₀) Filter.atTop (nhds v_star)h_fixed:IsFixedPoint v_star Tv_other:X →ᵇ ℝhv_other:IsFixedPoint v_other T⊢ v_other = v_starrightX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝhT:IsContraction Tv₀:X →ᵇ ℝhβ_ge0:0 ≤ hT.βh_cauchy:CauchySeq fun n ↦ T^[n] v₀v_star:X →ᵇ ℝh_lim:Filter.Tendsto (fun n ↦ T^[n] v₀) Filter.atTop (nhds v_star)h_fixed:IsFixedPoint v_star T⊢ ∀ (v_star : X →ᵇ ℝ), IsFixedPoint v_star T → ∀ (v₀ : X →ᵇ ℝ) (n : ℕ), dist v_star (T^[n] v₀) ≤ hT.β ^ n * dist v_star v₀
  change T v_other = v_other at hv_otherh.rightX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝhT:IsContraction Tv₀:X →ᵇ ℝhβ_ge0:0 ≤ hT.βh_cauchy:CauchySeq fun n ↦ T^[n] v₀v_star:X →ᵇ ℝh_lim:Filter.Tendsto (fun n ↦ T^[n] v₀) Filter.atTop (nhds v_star)h_fixed:IsFixedPoint v_star Tv_other:X →ᵇ ℝhv_other:T v_other = v_other⊢ v_other = v_starrightX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝhT:IsContraction Tv₀:X →ᵇ ℝhβ_ge0:0 ≤ hT.βh_cauchy:CauchySeq fun n ↦ T^[n] v₀v_star:X →ᵇ ℝh_lim:Filter.Tendsto (fun n ↦ T^[n] v₀) Filter.atTop (nhds v_star)h_fixed:IsFixedPoint v_star T⊢ ∀ (v_star : X →ᵇ ℝ), IsFixedPoint v_star T → ∀ (v₀ : X →ᵇ ℝ) (n : ℕ), dist v_star (T^[n] v₀) ≤ hT.β ^ n * dist v_star v₀  -- Apply the definition of the fixed point
  have h_fixed_eq : T v_star = v_star := h_fixedh.rightX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝhT:IsContraction Tv₀:X →ᵇ ℝhβ_ge0:0 ≤ hT.βh_cauchy:CauchySeq fun n ↦ T^[n] v₀v_star:X →ᵇ ℝh_lim:Filter.Tendsto (fun n ↦ T^[n] v₀) Filter.atTop (nhds v_star)h_fixed:IsFixedPoint v_star Tv_other:X →ᵇ ℝhv_other:T v_other = v_otherh_fixed_eq:T v_star = v_star⊢ v_other = v_starrightX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝhT:IsContraction Tv₀:X →ᵇ ℝhβ_ge0:0 ≤ hT.βh_cauchy:CauchySeq fun n ↦ T^[n] v₀v_star:X →ᵇ ℝh_lim:Filter.Tendsto (fun n ↦ T^[n] v₀) Filter.atTop (nhds v_star)h_fixed:IsFixedPoint v_star T⊢ ∀ (v_star : X →ᵇ ℝ), IsFixedPoint v_star T → ∀ (v₀ : X →ᵇ ℝ) (n : ℕ), dist v_star (T^[n] v₀) ≤ hT.β ^ n * dist v_star v₀
  have h_dist_zero : dist v_star v_other = 0 := byX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝhT:IsContraction T⊢ (∃! v_star, IsFixedPoint v_star T) ∧
  ∀ (v_star : X →ᵇ ℝ),
    IsFixedPoint v_star T → ∀ (v₀ : X →ᵇ ℝ) (n : ℕ), dist v_star (T^[n] v₀) ≤ hT.β ^ n * dist v_star v₀
    have h_le : dist v_star v_other ≤ hT.β * dist v_star v_other := byX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝhT:IsContraction T⊢ (∃! v_star, IsFixedPoint v_star T) ∧
  ∀ (v_star : X →ᵇ ℝ),
    IsFixedPoint v_star T → ∀ (v₀ : X →ᵇ ℝ) (n : ℕ), dist v_star (T^[n] v₀) ≤ hT.β ^ n * dist v_star v₀
      calc
        dist v_star v_other
        _ = dist (T v_star) (T v_other) :=
          byX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝhT:IsContraction Tv₀:X →ᵇ ℝhβ_ge0:0 ≤ hT.βh_cauchy:CauchySeq fun n ↦ T^[n] v₀v_star:X →ᵇ ℝh_lim:Filter.Tendsto (fun n ↦ T^[n] v₀) Filter.atTop (nhds v_star)h_fixed:IsFixedPoint v_star Tv_other:X →ᵇ ℝhv_other:T v_other = v_otherh_fixed_eq:T v_star = v_star⊢ dist v_star v_other = dist (T v_star) (T v_other) rw [h_fixed_eq, hv_other]All goals completed! 🐙
        _ ≤ hT.β * dist v_star v_other :=
          hT.h_dist v_star v_other
    have h_dis : 0 ≤ dist v_star v_other := dist_nonnegX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝhT:IsContraction Tv₀:X →ᵇ ℝhβ_ge0:0 ≤ hT.βh_cauchy:CauchySeq fun n ↦ T^[n] v₀v_star:X →ᵇ ℝh_lim:Filter.Tendsto (fun n ↦ T^[n] v₀) Filter.atTop (nhds v_star)h_fixed:IsFixedPoint v_star Tv_other:X →ᵇ ℝhv_other:T v_other = v_otherh_fixed_eq:T v_star = v_starh_le:dist v_star v_other ≤ hT.β * dist v_star v_otherh_dis:0 ≤ dist v_star v_other⊢ dist v_star v_other = 0
    by_contra h_posX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝhT:IsContraction Tv₀:X →ᵇ ℝhβ_ge0:0 ≤ hT.βh_cauchy:CauchySeq fun n ↦ T^[n] v₀v_star:X →ᵇ ℝh_lim:Filter.Tendsto (fun n ↦ T^[n] v₀) Filter.atTop (nhds v_star)h_fixed:IsFixedPoint v_star Tv_other:X →ᵇ ℝhv_other:T v_other = v_otherh_fixed_eq:T v_star = v_starh_le:dist v_star v_other ≤ hT.β * dist v_star v_otherh_dis:0 ≤ dist v_star v_otherh_pos:¬dist v_star v_other = 0⊢ False
    have h_gt : 0 < dist v_star v_other := lt_of_le_of_ne h_dis (Ne.symm h_pos)X:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝhT:IsContraction Tv₀:X →ᵇ ℝhβ_ge0:0 ≤ hT.βh_cauchy:CauchySeq fun n ↦ T^[n] v₀v_star:X →ᵇ ℝh_lim:Filter.Tendsto (fun n ↦ T^[n] v₀) Filter.atTop (nhds v_star)h_fixed:IsFixedPoint v_star Tv_other:X →ᵇ ℝhv_other:T v_other = v_otherh_fixed_eq:T v_star = v_starh_le:dist v_star v_other ≤ hT.β * dist v_star v_otherh_dis:0 ≤ dist v_star v_otherh_pos:¬dist v_star v_other = 0h_gt:0 < dist v_star v_other⊢ False  -- Combine less than or equal to with not equal to
    have h_lt : hT.β * dist v_star v_other < 1 * dist v_star v_other := mul_lt_mul_of_pos_right hT.hβ_lt1 h_gtX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝhT:IsContraction Tv₀:X →ᵇ ℝhβ_ge0:0 ≤ hT.βh_cauchy:CauchySeq fun n ↦ T^[n] v₀v_star:X →ᵇ ℝh_lim:Filter.Tendsto (fun n ↦ T^[n] v₀) Filter.atTop (nhds v_star)h_fixed:IsFixedPoint v_star Tv_other:X →ᵇ ℝhv_other:T v_other = v_otherh_fixed_eq:T v_star = v_starh_le:dist v_star v_other ≤ hT.β * dist v_star v_otherh_dis:0 ≤ dist v_star v_otherh_pos:¬dist v_star v_other = 0h_gt:0 < dist v_star v_otherh_lt:hT.β * dist v_star v_other < 1 * dist v_star v_other⊢ False
    rw [one_mul] at h_ltX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝhT:IsContraction Tv₀:X →ᵇ ℝhβ_ge0:0 ≤ hT.βh_cauchy:CauchySeq fun n ↦ T^[n] v₀v_star:X →ᵇ ℝh_lim:Filter.Tendsto (fun n ↦ T^[n] v₀) Filter.atTop (nhds v_star)h_fixed:IsFixedPoint v_star Tv_other:X →ᵇ ℝhv_other:T v_other = v_otherh_fixed_eq:T v_star = v_starh_le:dist v_star v_other ≤ hT.β * dist v_star v_otherh_dis:0 ≤ dist v_star v_otherh_pos:¬dist v_star v_other = 0h_gt:0 < dist v_star v_otherh_lt:hT.β * dist v_star v_other < dist v_star v_other⊢ False
    linarithAll goals completed! 🐙
  exact (dist_eq_zero.mp h_dist_zero).symmrightX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝhT:IsContraction Tv₀:X →ᵇ ℝhβ_ge0:0 ≤ hT.βh_cauchy:CauchySeq fun n ↦ T^[n] v₀v_star:X →ᵇ ℝh_lim:Filter.Tendsto (fun n ↦ T^[n] v₀) Filter.atTop (nhds v_star)h_fixed:IsFixedPoint v_star T⊢ ∀ (v_star : X →ᵇ ℝ), IsFixedPoint v_star T → ∀ (v₀ : X →ᵇ ℝ) (n : ℕ), dist v_star (T^[n] v₀) ≤ hT.β ^ n * dist v_star v₀
  -- (b)
  -- use β  -- Use the β we have defined as the candidate existence (the witness)
  -- refine ⟨hβ_gt0, hβ_lt1, ?_⟩  -- Tell Lean to prove the third part now
  intro v_star' hv_star'rightX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝhT:IsContraction Tv₀:X →ᵇ ℝhβ_ge0:0 ≤ hT.βh_cauchy:CauchySeq fun n ↦ T^[n] v₀v_star:X →ᵇ ℝh_lim:Filter.Tendsto (fun n ↦ T^[n] v₀) Filter.atTop (nhds v_star)h_fixed:IsFixedPoint v_star Tv_star':X →ᵇ ℝhv_star':IsFixedPoint v_star' T⊢ ∀ (v₀ : X →ᵇ ℝ) (n : ℕ), dist v_star' (T^[n] v₀) ≤ hT.β ^ n * dist v_star' v₀ v₀'rightX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝhT:IsContraction Tv₀:X →ᵇ ℝhβ_ge0:0 ≤ hT.βh_cauchy:CauchySeq fun n ↦ T^[n] v₀v_star:X →ᵇ ℝh_lim:Filter.Tendsto (fun n ↦ T^[n] v₀) Filter.atTop (nhds v_star)h_fixed:IsFixedPoint v_star Tv_star':X →ᵇ ℝhv_star':IsFixedPoint v_star' Tv₀':X →ᵇ ℝ⊢ ∀ (n : ℕ), dist v_star' (T^[n] v₀') ≤ hT.β ^ n * dist v_star' v₀' nrightX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝhT:IsContraction Tv₀:X →ᵇ ℝhβ_ge0:0 ≤ hT.βh_cauchy:CauchySeq fun n ↦ T^[n] v₀v_star:X →ᵇ ℝh_lim:Filter.Tendsto (fun n ↦ T^[n] v₀) Filter.atTop (nhds v_star)h_fixed:IsFixedPoint v_star Tv_star':X →ᵇ ℝhv_star':IsFixedPoint v_star' Tv₀':X →ᵇ ℝn:ℕ⊢ dist v_star' (T^[n] v₀') ≤ hT.β ^ n * dist v_star' v₀'
  change T v_star' = v_star' at hv_star'rightX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝhT:IsContraction Tv₀:X →ᵇ ℝhβ_ge0:0 ≤ hT.βh_cauchy:CauchySeq fun n ↦ T^[n] v₀v_star:X →ᵇ ℝh_lim:Filter.Tendsto (fun n ↦ T^[n] v₀) Filter.atTop (nhds v_star)h_fixed:IsFixedPoint v_star Tv_star':X →ᵇ ℝv₀':X →ᵇ ℝn:ℕhv_star':T v_star' = v_star'⊢ dist v_star' (T^[n] v₀') ≤ hT.β ^ n * dist v_star' v₀'  -- Apply the fixed point definition
  induction n with
  | zero =>right.zeroX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝhT:IsContraction Tv₀:X →ᵇ ℝhβ_ge0:0 ≤ hT.βh_cauchy:CauchySeq fun n ↦ T^[n] v₀v_star:X →ᵇ ℝh_lim:Filter.Tendsto (fun n ↦ T^[n] v₀) Filter.atTop (nhds v_star)h_fixed:IsFixedPoint v_star Tv_star':X →ᵇ ℝv₀':X →ᵇ ℝhv_star':T v_star' = v_star'⊢ dist v_star' (T^[0] v₀') ≤ hT.β ^ 0 * dist v_star' v₀'
    rw [pow_zero, one_mul]right.zeroX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝhT:IsContraction Tv₀:X →ᵇ ℝhβ_ge0:0 ≤ hT.βh_cauchy:CauchySeq fun n ↦ T^[n] v₀v_star:X →ᵇ ℝh_lim:Filter.Tendsto (fun n ↦ T^[n] v₀) Filter.atTop (nhds v_star)h_fixed:IsFixedPoint v_star Tv_star':X →ᵇ ℝv₀':X →ᵇ ℝhv_star':T v_star' = v_star'⊢ dist v_star' (T^[0] v₀') ≤ dist v_star' v₀'
    rflAll goals completed! 🐙
  | succ k ih =>right.succX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝhT:IsContraction Tv₀:X →ᵇ ℝhβ_ge0:0 ≤ hT.βh_cauchy:CauchySeq fun n ↦ T^[n] v₀v_star:X →ᵇ ℝh_lim:Filter.Tendsto (fun n ↦ T^[n] v₀) Filter.atTop (nhds v_star)h_fixed:IsFixedPoint v_star Tv_star':X →ᵇ ℝv₀':X →ᵇ ℝhv_star':T v_star' = v_star'k:ℕih:dist v_star' (T^[k] v₀') ≤ hT.β ^ k * dist v_star' v₀'⊢ dist v_star' (T^[k + 1] v₀') ≤ hT.β ^ (k + 1) * dist v_star' v₀'
    calc
      dist v_star' (T^[k + 1] v₀')
      _ = dist (T v_star') (T (T^[k] v₀')) :=
        byX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝhT:IsContraction Tv₀:X →ᵇ ℝhβ_ge0:0 ≤ hT.βh_cauchy:CauchySeq fun n ↦ T^[n] v₀v_star:X →ᵇ ℝh_lim:Filter.Tendsto (fun n ↦ T^[n] v₀) Filter.atTop (nhds v_star)h_fixed:IsFixedPoint v_star Tv_star':X →ᵇ ℝv₀':X →ᵇ ℝhv_star':T v_star' = v_star'k:ℕih:dist v_star' (T^[k] v₀') ≤ hT.β ^ k * dist v_star' v₀'⊢ dist v_star' (T^[k + 1] v₀') = dist (T v_star') (T (T^[k] v₀')) rw [hv_star', Function.iterate_succ_apply']All goals completed! 🐙
      _ ≤ hT.β * dist v_star' (T^[k] v₀') :=
        hT.h_dist v_star' (T^[k] v₀')
      _ ≤ hT.β * (hT.β^k * dist v_star' v₀') :=
        mul_le_mul_of_nonneg_left ih hβ_ge0
      _ = hT.β^(k + 1) * dist v_star' v₀' := byX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝhT:IsContraction Tv₀:X →ᵇ ℝhβ_ge0:0 ≤ hT.βh_cauchy:CauchySeq fun n ↦ T^[n] v₀v_star:X →ᵇ ℝh_lim:Filter.Tendsto (fun n ↦ T^[n] v₀) Filter.atTop (nhds v_star)h_fixed:IsFixedPoint v_star Tv_star':X →ᵇ ℝv₀':X →ᵇ ℝhv_star':T v_star' = v_star'k:ℕih:dist v_star' (T^[k] v₀') ≤ hT.β ^ k * dist v_star' v₀'⊢ hT.β * (hT.β ^ k * dist v_star' v₀') = hT.β ^ (k + 1) * dist v_star' v₀'
        ringAll goals completed! 🐙

We can now provide a theorem that will tell us what sufficient conditions are for an operator to be a contraction mapping. That will help one find contraction mappings, for which one can use the results of the Contraction Mapping Theorem.

First, we will need to define two properties an operator can have.

Definition: Monotonicity

An operator T is said to satisfy monotonicity if for all bounded continuous functions f, g : X → ℝ such that f(x) ≤ g(x) ∀ x ∈ X, we have T f(x) ≤ T g(x).

def MonotoneOperator (T : (X →ᵇ ℝ) → (X →ᵇ ℝ)) : Prop :=
  ∀ f g : X →ᵇ ℝ, f ≤ g → T f ≤ T g

Definition: Discounting

An operator T is said to satisfy discounting when for all a ∈ ℝ_+, and for all x ∈ X we have that T (f(x) + a) ≤ T f(x) + β a.

def DiscountingOperator (T : (X →ᵇ ℝ) → (X →ᵇ ℝ)) (β : ℝ) : Prop :=
  0 < β ∧ β < 1 ∧ ∀ (f : X →ᵇ ℝ) (a : ℝ), 0 ≤ a → T (f + const X a) ≤ T f + const X (β * a)

Theorem: Blackwell's Sufficient Conditions

Let X ⊆ ℝ^L and B(X) be the space of bounded functions f: X → ℝ with d being the sup-norm. Let T : B(X) → B(X) be an operator satisfying the following two conditions.

Monotonicity. If f, g ∈ B(X) are such that f(x) ≤ g(x) for all x ∈ X, then (Tf)(x) ≤ (Tg)(x) for all x ∈ X.
Discounting. Let the function f + a, for f ∈ B(X) and a ∈ ℝ_+, be defined by (f + a)(x) = f(x) + a. There exists β ∈ (0, 1) such that for all f ∈ B(X), 0 ≤ a, and all x ∈ X we have the following. [T(f + a)](x) ≤ [Tf](x) + β a. Proof.
For f, g ∈ B(X), denote f ≤ g when f(x) ≤ g(x) for all x ∈ X. We must have that for all x ∈ X, we have that f(x) - g(x) ≤ sup_{y ∈ X} \lVert f(y) - g(y) \rVert =: d(f, g). We can therefore write f ≤ g + d(f, g) by the notation introduced at the start of this proof. From monotonicity, we obtain that Tf ≤ T[g + d(f, g)]. As d(f, g) ∈ ℝ_+, we have that Tf ≤ Tg + βd(f, g) for some β ∈ (0, 1). Rearranging yields Tf - Tg ≤ β d(f, g). Repeating this argument while switching positions for f and g yields Tg - Tf ≤ β d(g, f), or -(Tf - Tg) ≤ β d(f, g) by symmetry of the metric. Thus, we obtain the definition of T being a contraction mapping as stated below. sup_{x ∈ X} \lVert (Tf)(x) - (Tg)(x) \rVert = d(Tf, Tg) ≤ β d(f, g). ■

def blackwell_sufficient_conditions (T : BoundedContinuousFunction X ℝ → BoundedContinuousFunction X ℝ)
  (β : ℝ) (h_mono : MonotoneOperator T) (h_disc : DiscountingOperator T β) :
  IsContraction T where
  β := β
  hβ_gt0 := h_disc.1  -- Assign first group
  hβ_lt1 := h_disc.2.1  -- Assign first of second group
  h_dist := byX:Type u_1inst✝¹:Nonempty Xinst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝβ:ℝh_mono:MonotoneOperator Th_disc:DiscountingOperator T β⊢ ∀ (f g : X →ᵇ ℝ), dist (T f) (T g) ≤ β * dist f g  -- Supply the last property by a proof
    intro f gX:Type u_1inst✝¹:Nonempty Xinst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝβ:ℝh_mono:MonotoneOperator Th_disc:DiscountingOperator T βf:X →ᵇ ℝg:X →ᵇ ℝ⊢ dist (T f) (T g) ≤ β * dist f g
    -- Transform the sup-norm inequality into a pointwise one
    rw [dist_le_iff_of_nonempty]X:Type u_1inst✝¹:Nonempty Xinst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝβ:ℝh_mono:MonotoneOperator Th_disc:DiscountingOperator T βf:X →ᵇ ℝg:X →ᵇ ℝ⊢ ∀ (x : X), dist ((T f) x) ((T g) x) ≤ β * dist f g
    intro xX:Type u_1inst✝¹:Nonempty Xinst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝβ:ℝh_mono:MonotoneOperator Th_disc:DiscountingOperator T βf:X →ᵇ ℝg:X →ᵇ ℝx:X⊢ dist ((T f) x) ((T g) x) ≤ β * dist f g
    -- Prove that `f ≤ g + dist(f, g)` pointwise
    have h_le_g : f ≤ g + const X (dist f g) := byX:Type u_1inst✝¹:Nonempty Xinst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝβ:ℝh_mono:MonotoneOperator Th_disc:DiscountingOperator T β⊢ ∀ (f g : X →ᵇ ℝ), dist (T f) (T g) ≤ β * dist f g
      intro yX:Type u_1inst✝¹:Nonempty Xinst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝβ:ℝh_mono:MonotoneOperator Th_disc:DiscountingOperator T βf:X →ᵇ ℝg:X →ᵇ ℝx:Xy:X⊢ (fun f ↦ f.toFun) f y ≤ (fun f ↦ f.toFun) (g + const X (dist f g)) y
      -- In `dist f g ≤ C ↔ ∀ (x : α), dist (f x) (g x) ≤ C`, set `C = dist f g`
      have hy := (dist_le_iff_of_nonempty.mp (le_refl (dist f g))) yX:Type u_1inst✝¹:Nonempty Xinst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝβ:ℝh_mono:MonotoneOperator Th_disc:DiscountingOperator T βf:X →ᵇ ℝg:X →ᵇ ℝx:Xy:Xhy:dist (f y) (g y) ≤ dist f g⊢ (fun f ↦ f.toFun) f y ≤ (fun f ↦ f.toFun) (g + const X (dist f g)) y
      rw [Real.dist_eq] at hyX:Type u_1inst✝¹:Nonempty Xinst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝβ:ℝh_mono:MonotoneOperator Th_disc:DiscountingOperator T βf:X →ᵇ ℝg:X →ᵇ ℝx:Xy:Xhy:|f y - g y| ≤ dist f g⊢ (fun f ↦ f.toFun) f y ≤ (fun f ↦ f.toFun) (g + const X (dist f g)) y
      have h_abs := le_abs_self (f y - g y)X:Type u_1inst✝¹:Nonempty Xinst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝβ:ℝh_mono:MonotoneOperator Th_disc:DiscountingOperator T βf:X →ᵇ ℝg:X →ᵇ ℝx:Xy:Xhy:|f y - g y| ≤ dist f gh_abs:f y - g y ≤ |f y - g y|⊢ (fun f ↦ f.toFun) f y ≤ (fun f ↦ f.toFun) (g + const X (dist f g)) y
      have h_combined := le_trans h_abs hyX:Type u_1inst✝¹:Nonempty Xinst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝβ:ℝh_mono:MonotoneOperator Th_disc:DiscountingOperator T βf:X →ᵇ ℝg:X →ᵇ ℝx:Xy:Xhy:|f y - g y| ≤ dist f gh_abs:f y - g y ≤ |f y - g y|h_combined:f y - g y ≤ dist f g⊢ (fun f ↦ f.toFun) f y ≤ (fun f ↦ f.toFun) (g + const X (dist f g)) y
      change f y ≤ g y + dist f gX:Type u_1inst✝¹:Nonempty Xinst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝβ:ℝh_mono:MonotoneOperator Th_disc:DiscountingOperator T βf:X →ᵇ ℝg:X →ᵇ ℝx:Xy:Xhy:|f y - g y| ≤ dist f gh_abs:f y - g y ≤ |f y - g y|h_combined:f y - g y ≤ dist f g⊢ f y ≤ g y + dist f g
      exact sub_le_iff_le_add'.mp h_combinedAll goals completed! 🐙
    -- Apply monotonicity and discounting to get the first bound
    have h_T_le1 := h_mono f (g + const X (dist f g)) h_le_gX:Type u_1inst✝¹:Nonempty Xinst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝβ:ℝh_mono:MonotoneOperator Th_disc:DiscountingOperator T βf:X →ᵇ ℝg:X →ᵇ ℝx:Xh_le_g:f ≤ g + const X (dist f g)h_T_le1:T f ≤ T (g + const X (dist f g))⊢ dist ((T f) x) ((T g) x) ≤ β * dist f g
    have h_disc1 := h_disc.2.2 g (dist f g) dist_nonnegX:Type u_1inst✝¹:Nonempty Xinst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝβ:ℝh_mono:MonotoneOperator Th_disc:DiscountingOperator T βf:X →ᵇ ℝg:X →ᵇ ℝx:Xh_le_g:f ≤ g + const X (dist f g)h_T_le1:T f ≤ T (g + const X (dist f g))h_disc1:T (g + const X (dist f g)) ≤ T g + const X (β * dist f g)⊢ dist ((T f) x) ((T g) x) ≤ β * dist f g
    have h_combined1 := le_trans h_T_le1 h_disc1X:Type u_1inst✝¹:Nonempty Xinst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝβ:ℝh_mono:MonotoneOperator Th_disc:DiscountingOperator T βf:X →ᵇ ℝg:X →ᵇ ℝx:Xh_le_g:f ≤ g + const X (dist f g)h_T_le1:T f ≤ T (g + const X (dist f g))h_disc1:T (g + const X (dist f g)) ≤ T g + const X (β * dist f g)h_combined1:T f ≤ T g + const X (β * dist f g)⊢ dist ((T f) x) ((T g) x) ≤ β * dist f g
    have h_x1 := h_combined1 xX:Type u_1inst✝¹:Nonempty Xinst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝβ:ℝh_mono:MonotoneOperator Th_disc:DiscountingOperator T βf:X →ᵇ ℝg:X →ᵇ ℝx:Xh_le_g:f ≤ g + const X (dist f g)h_T_le1:T f ≤ T (g + const X (dist f g))h_disc1:T (g + const X (dist f g)) ≤ T g + const X (β * dist f g)h_combined1:T f ≤ T g + const X (β * dist f g)h_x1:(fun f ↦ f.toFun) (T f) x ≤ (fun f ↦ f.toFun) (T g + const X (β * dist f g)) x⊢ dist ((T f) x) ((T g) x) ≤ β * dist f g
    -- Prove that `g ≤ f + dist(g, f))` pointwise
    have h_le_f : g ≤ f + const X (dist g f) := byX:Type u_1inst✝¹:Nonempty Xinst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝβ:ℝh_mono:MonotoneOperator Th_disc:DiscountingOperator T β⊢ ∀ (f g : X →ᵇ ℝ), dist (T f) (T g) ≤ β * dist f g
      intro yX:Type u_1inst✝¹:Nonempty Xinst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝβ:ℝh_mono:MonotoneOperator Th_disc:DiscountingOperator T βf:X →ᵇ ℝg:X →ᵇ ℝx:Xh_le_g:f ≤ g + const X (dist f g)h_T_le1:T f ≤ T (g + const X (dist f g))h_disc1:T (g + const X (dist f g)) ≤ T g + const X (β * dist f g)h_combined1:T f ≤ T g + const X (β * dist f g)h_x1:(fun f ↦ f.toFun) (T f) x ≤ (fun f ↦ f.toFun) (T g + const X (β * dist f g)) xy:X⊢ (fun f ↦ f.toFun) g y ≤ (fun f ↦ f.toFun) (f + const X (dist g f)) y
      have hy := (dist_le_iff_of_nonempty.mp (le_refl (dist g f))) yX:Type u_1inst✝¹:Nonempty Xinst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝβ:ℝh_mono:MonotoneOperator Th_disc:DiscountingOperator T βf:X →ᵇ ℝg:X →ᵇ ℝx:Xh_le_g:f ≤ g + const X (dist f g)h_T_le1:T f ≤ T (g + const X (dist f g))h_disc1:T (g + const X (dist f g)) ≤ T g + const X (β * dist f g)h_combined1:T f ≤ T g + const X (β * dist f g)h_x1:(fun f ↦ f.toFun) (T f) x ≤ (fun f ↦ f.toFun) (T g + const X (β * dist f g)) xy:Xhy:dist (g y) (f y) ≤ dist g f⊢ (fun f ↦ f.toFun) g y ≤ (fun f ↦ f.toFun) (f + const X (dist g f)) y
      rw [Real.dist_eq] at hyX:Type u_1inst✝¹:Nonempty Xinst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝβ:ℝh_mono:MonotoneOperator Th_disc:DiscountingOperator T βf:X →ᵇ ℝg:X →ᵇ ℝx:Xh_le_g:f ≤ g + const X (dist f g)h_T_le1:T f ≤ T (g + const X (dist f g))h_disc1:T (g + const X (dist f g)) ≤ T g + const X (β * dist f g)h_combined1:T f ≤ T g + const X (β * dist f g)h_x1:(fun f ↦ f.toFun) (T f) x ≤ (fun f ↦ f.toFun) (T g + const X (β * dist f g)) xy:Xhy:|g y - f y| ≤ dist g f⊢ (fun f ↦ f.toFun) g y ≤ (fun f ↦ f.toFun) (f + const X (dist g f)) y
      have h_abs := le_abs_self (g y - f y)X:Type u_1inst✝¹:Nonempty Xinst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝβ:ℝh_mono:MonotoneOperator Th_disc:DiscountingOperator T βf:X →ᵇ ℝg:X →ᵇ ℝx:Xh_le_g:f ≤ g + const X (dist f g)h_T_le1:T f ≤ T (g + const X (dist f g))h_disc1:T (g + const X (dist f g)) ≤ T g + const X (β * dist f g)h_combined1:T f ≤ T g + const X (β * dist f g)h_x1:(fun f ↦ f.toFun) (T f) x ≤ (fun f ↦ f.toFun) (T g + const X (β * dist f g)) xy:Xhy:|g y - f y| ≤ dist g fh_abs:g y - f y ≤ |g y - f y|⊢ (fun f ↦ f.toFun) g y ≤ (fun f ↦ f.toFun) (f + const X (dist g f)) y
      have h_combined := le_trans h_abs hyX:Type u_1inst✝¹:Nonempty Xinst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝβ:ℝh_mono:MonotoneOperator Th_disc:DiscountingOperator T βf:X →ᵇ ℝg:X →ᵇ ℝx:Xh_le_g:f ≤ g + const X (dist f g)h_T_le1:T f ≤ T (g + const X (dist f g))h_disc1:T (g + const X (dist f g)) ≤ T g + const X (β * dist f g)h_combined1:T f ≤ T g + const X (β * dist f g)h_x1:(fun f ↦ f.toFun) (T f) x ≤ (fun f ↦ f.toFun) (T g + const X (β * dist f g)) xy:Xhy:|g y - f y| ≤ dist g fh_abs:g y - f y ≤ |g y - f y|h_combined:g y - f y ≤ dist g f⊢ (fun f ↦ f.toFun) g y ≤ (fun f ↦ f.toFun) (f + const X (dist g f)) y
      change g y ≤ f y + dist g fX:Type u_1inst✝¹:Nonempty Xinst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝβ:ℝh_mono:MonotoneOperator Th_disc:DiscountingOperator T βf:X →ᵇ ℝg:X →ᵇ ℝx:Xh_le_g:f ≤ g + const X (dist f g)h_T_le1:T f ≤ T (g + const X (dist f g))h_disc1:T (g + const X (dist f g)) ≤ T g + const X (β * dist f g)h_combined1:T f ≤ T g + const X (β * dist f g)h_x1:(fun f ↦ f.toFun) (T f) x ≤ (fun f ↦ f.toFun) (T g + const X (β * dist f g)) xy:Xhy:|g y - f y| ≤ dist g fh_abs:g y - f y ≤ |g y - f y|h_combined:g y - f y ≤ dist g f⊢ g y ≤ f y + dist g f
      exact sub_le_iff_le_add'.mp h_combinedAll goals completed! 🐙
    -- Apply monotonicity and discounting to get the second bound
    have h_T_le2 := h_mono g (f + const X (dist g f)) h_le_fX:Type u_1inst✝¹:Nonempty Xinst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝβ:ℝh_mono:MonotoneOperator Th_disc:DiscountingOperator T βf:X →ᵇ ℝg:X →ᵇ ℝx:Xh_le_g:f ≤ g + const X (dist f g)h_T_le1:T f ≤ T (g + const X (dist f g))h_disc1:T (g + const X (dist f g)) ≤ T g + const X (β * dist f g)h_combined1:T f ≤ T g + const X (β * dist f g)h_x1:(fun f ↦ f.toFun) (T f) x ≤ (fun f ↦ f.toFun) (T g + const X (β * dist f g)) xh_le_f:g ≤ f + const X (dist g f)h_T_le2:T g ≤ T (f + const X (dist g f))⊢ dist ((T f) x) ((T g) x) ≤ β * dist f g
    have h_disc2 := h_disc.2.2 f (dist g f) dist_nonnegX:Type u_1inst✝¹:Nonempty Xinst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝβ:ℝh_mono:MonotoneOperator Th_disc:DiscountingOperator T βf:X →ᵇ ℝg:X →ᵇ ℝx:Xh_le_g:f ≤ g + const X (dist f g)h_T_le1:T f ≤ T (g + const X (dist f g))h_disc1:T (g + const X (dist f g)) ≤ T g + const X (β * dist f g)h_combined1:T f ≤ T g + const X (β * dist f g)h_x1:(fun f ↦ f.toFun) (T f) x ≤ (fun f ↦ f.toFun) (T g + const X (β * dist f g)) xh_le_f:g ≤ f + const X (dist g f)h_T_le2:T g ≤ T (f + const X (dist g f))h_disc2:T (f + const X (dist g f)) ≤ T f + const X (β * dist g f)⊢ dist ((T f) x) ((T g) x) ≤ β * dist f g
    have h_combined2 := le_trans h_T_le2 h_disc2X:Type u_1inst✝¹:Nonempty Xinst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝβ:ℝh_mono:MonotoneOperator Th_disc:DiscountingOperator T βf:X →ᵇ ℝg:X →ᵇ ℝx:Xh_le_g:f ≤ g + const X (dist f g)h_T_le1:T f ≤ T (g + const X (dist f g))h_disc1:T (g + const X (dist f g)) ≤ T g + const X (β * dist f g)h_combined1:T f ≤ T g + const X (β * dist f g)h_x1:(fun f ↦ f.toFun) (T f) x ≤ (fun f ↦ f.toFun) (T g + const X (β * dist f g)) xh_le_f:g ≤ f + const X (dist g f)h_T_le2:T g ≤ T (f + const X (dist g f))h_disc2:T (f + const X (dist g f)) ≤ T f + const X (β * dist g f)h_combined2:T g ≤ T f + const X (β * dist g f)⊢ dist ((T f) x) ((T g) x) ≤ β * dist f g
    have h_x2 := h_combined2 xX:Type u_1inst✝¹:Nonempty Xinst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝβ:ℝh_mono:MonotoneOperator Th_disc:DiscountingOperator T βf:X →ᵇ ℝg:X →ᵇ ℝx:Xh_le_g:f ≤ g + const X (dist f g)h_T_le1:T f ≤ T (g + const X (dist f g))h_disc1:T (g + const X (dist f g)) ≤ T g + const X (β * dist f g)h_combined1:T f ≤ T g + const X (β * dist f g)h_x1:(fun f ↦ f.toFun) (T f) x ≤ (fun f ↦ f.toFun) (T g + const X (β * dist f g)) xh_le_f:g ≤ f + const X (dist g f)h_T_le2:T g ≤ T (f + const X (dist g f))h_disc2:T (f + const X (dist g f)) ≤ T f + const X (β * dist g f)h_combined2:T g ≤ T f + const X (β * dist g f)h_x2:(fun f ↦ f.toFun) (T g) x ≤ (fun f ↦ f.toFun) (T f + const X (β * dist g f)) x⊢ dist ((T f) x) ((T g) x) ≤ β * dist f g
    -- Reduce the lambda function expressions and the const function expression
    simp at h_x1 h_x2X:Type u_1inst✝¹:Nonempty Xinst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝβ:ℝh_mono:MonotoneOperator Th_disc:DiscountingOperator T βf:X →ᵇ ℝg:X →ᵇ ℝx:Xh_le_g:f ≤ g + const X (dist f g)h_T_le1:T f ≤ T (g + const X (dist f g))h_disc1:T (g + const X (dist f g)) ≤ T g + const X (β * dist f g)h_combined1:T f ≤ T g + const X (β * dist f g)h_x1:(T f) x ≤ (T g) x + β * dist f gh_le_f:g ≤ f + const X (dist g f)h_T_le2:T g ≤ T (f + const X (dist g f))h_disc2:T (f + const X (dist g f)) ≤ T f + const X (β * dist g f)h_combined2:T g ≤ T f + const X (β * dist g f)h_x2:(T g) x ≤ (T f) x + β * dist g f⊢ dist ((T f) x) ((T g) x) ≤ β * dist f g
    -- Apply commutativity of the second inequality to then conclude
    -- the result using metric properties of ℝ (dist x y = |x - y|)
    -- and the definition of |x - y| ≤ c → x - y ≤ c ∧ -(x - y) ≤ c
    rw [dist_comm g f] at h_x2X:Type u_1inst✝¹:Nonempty Xinst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝβ:ℝh_mono:MonotoneOperator Th_disc:DiscountingOperator T βf:X →ᵇ ℝg:X →ᵇ ℝx:Xh_le_g:f ≤ g + const X (dist f g)h_T_le1:T f ≤ T (g + const X (dist f g))h_disc1:T (g + const X (dist f g)) ≤ T g + const X (β * dist f g)h_combined1:T f ≤ T g + const X (β * dist f g)h_x1:(T f) x ≤ (T g) x + β * dist f gh_le_f:g ≤ f + const X (dist g f)h_T_le2:T g ≤ T (f + const X (dist g f))h_disc2:T (f + const X (dist g f)) ≤ T f + const X (β * dist g f)h_combined2:T g ≤ T f + const X (β * dist g f)h_x2:(T g) x ≤ (T f) x + β * dist f g⊢ dist ((T f) x) ((T g) x) ≤ β * dist f g
    rw [Real.dist_eq]X:Type u_1inst✝¹:Nonempty Xinst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝβ:ℝh_mono:MonotoneOperator Th_disc:DiscountingOperator T βf:X →ᵇ ℝg:X →ᵇ ℝx:Xh_le_g:f ≤ g + const X (dist f g)h_T_le1:T f ≤ T (g + const X (dist f g))h_disc1:T (g + const X (dist f g)) ≤ T g + const X (β * dist f g)h_combined1:T f ≤ T g + const X (β * dist f g)h_x1:(T f) x ≤ (T g) x + β * dist f gh_le_f:g ≤ f + const X (dist g f)h_T_le2:T g ≤ T (f + const X (dist g f))h_disc2:T (f + const X (dist g f)) ≤ T f + const X (β * dist g f)h_combined2:T g ≤ T f + const X (β * dist g f)h_x2:(T g) x ≤ (T f) x + β * dist f g⊢ |(T f) x - (T g) x| ≤ β * dist f g
    rw [add_comm, ← sub_le_iff_le_add] at h_x1 h_x2X:Type u_1inst✝¹:Nonempty Xinst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝβ:ℝh_mono:MonotoneOperator Th_disc:DiscountingOperator T βf:X →ᵇ ℝg:X →ᵇ ℝx:Xh_le_g:f ≤ g + const X (dist f g)h_T_le1:T f ≤ T (g + const X (dist f g))h_disc1:T (g + const X (dist f g)) ≤ T g + const X (β * dist f g)h_combined1:T f ≤ T g + const X (β * dist f g)h_x1:(T f) x - (T g) x ≤ β * dist f gh_le_f:g ≤ f + const X (dist g f)h_T_le2:T g ≤ T (f + const X (dist g f))h_disc2:T (f + const X (dist g f)) ≤ T f + const X (β * dist g f)h_combined2:T g ≤ T f + const X (β * dist g f)h_x2:(T g) x - (T f) x ≤ β * dist f g⊢ |(T f) x - (T g) x| ≤ β * dist f g
    rw [← neg_sub] at h_x2X:Type u_1inst✝¹:Nonempty Xinst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝβ:ℝh_mono:MonotoneOperator Th_disc:DiscountingOperator T βf:X →ᵇ ℝg:X →ᵇ ℝx:Xh_le_g:f ≤ g + const X (dist f g)h_T_le1:T f ≤ T (g + const X (dist f g))h_disc1:T (g + const X (dist f g)) ≤ T g + const X (β * dist f g)h_combined1:T f ≤ T g + const X (β * dist f g)h_x1:(T f) x - (T g) x ≤ β * dist f gh_le_f:g ≤ f + const X (dist g f)h_T_le2:T g ≤ T (f + const X (dist g f))h_disc2:T (f + const X (dist g f)) ≤ T f + const X (β * dist g f)h_combined2:T g ≤ T f + const X (β * dist g f)h_x2:-((T f) x - (T g) x) ≤ β * dist f g⊢ |(T f) x - (T g) x| ≤ β * dist f g
    exact abs_le.mpr ⟨neg_le.mp h_x2, h_x1⟩All goals completed! 🐙

Appendix

This appendix contains several results I proved but ended up not needing. The first proves that d(T^{n + k} v_0, T^n v_0) ≤ ∑_{i = 0}^{k - 1} d(T^{n + i} v_0, T^{n + i + 1} v_0), while the second proves that d(T^{n + k} v_0, T^n v_0) ≤ d(T v_0, v_0)) β^n / (1 - β), continuing previously defined notation. Chaining these lemmas together in that order would allow one to conclude that d(T^{n + k} v_0, T^n v_0) ≤ d(T v_0, v_0)) β^n / (1 - β), which provides an alternative avenue to proving (T^{n} v)_{n = 0}^∞ is a Cauchy sequence.

Lemma: Bound Arbitrary Difference Expanded

∀ n, k ∈ ℕ, ∀ v ∈ B(X),\ d(T^n v, T^{n + k} v) ≤ ∑_{i = 1}^k d(T^{n + i - 1} v, T^{n + i} v) Proof.
Apply induction with the triangle inequality. d(T^n v, T^{n + k} v) ≤ d(T^n v, T^{n + 1} v) + d(T^{n + 1} v, T^{n + k} v) From this, it follows that d(T^n v, T^{n + k} v) ≤ d(T^n v, T^{n + 1} v) + d(T^{n + 1} v, T^{n + 2} v) + … + d(T^{n + k - 1} v, T^{n + k} v). ■

omit [Nonempty X] in
lemma bound_difference_arbitrary_expanded {T : BoundedContinuousFunction X ℝ → BoundedContinuousFunction X ℝ} {v₀ : BoundedContinuousFunction X ℝ} :
∀ (n : ℕ) (k : ℕ), dist (T^[n] v₀) (T^[n + k] v₀) ≤ ∑ i ∈ Finset.range k, dist (T^[n + i] v₀) (T^[n + i + 1] v₀) := byX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝv₀:X →ᵇ ℝ⊢ ∀ (n k : ℕ), dist (T^[n] v₀) (T^[n + k] v₀) ≤ ∑ i ∈ Finset.range k, dist (T^[n + i] v₀) (T^[n + i + 1] v₀)
  intro n kX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝv₀:X →ᵇ ℝn:ℕk:ℕ⊢ dist (T^[n] v₀) (T^[n + k] v₀) ≤ ∑ i ∈ Finset.range k, dist (T^[n + i] v₀) (T^[n + i + 1] v₀)
  induction k with
  | zero =>zeroX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝv₀:X →ᵇ ℝn:ℕ⊢ dist (T^[n] v₀) (T^[n + 0] v₀) ≤ ∑ i ∈ Finset.range 0, dist (T^[n + i] v₀) (T^[n + i + 1] v₀)
      simp [dist_self]All goals completed! 🐙
  | succ k ih =>succX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝv₀:X →ᵇ ℝn:ℕk:ℕih:dist (T^[n] v₀) (T^[n + k] v₀) ≤ ∑ i ∈ Finset.range k, dist (T^[n + i] v₀) (T^[n + i + 1] v₀)⊢ dist (T^[n] v₀) (T^[n + (k + 1)] v₀) ≤ ∑ i ∈ Finset.range (k + 1), dist (T^[n + i] v₀) (T^[n + i + 1] v₀)
      calc
        dist (T^[n] v₀) (T^[n + k + 1] v₀)
        _ ≤ dist (T^[n] v₀) (T^[n + k] v₀) + dist (T^[n + k] v₀) (T^[n + k + 1] v₀) :=
          -- Apply the triangle inequality
          dist_triangle _ _ _
        _ ≤ (∑ i ∈ Finset.range k, dist (T^[n + i] v₀) (T^[n + i + 1] v₀)) + dist (T^[n + k] v₀) (T^[n + k + 1] v₀) :=
          add_le_add_left ih _
        _ = ∑ i ∈ Finset.range (k + 1), dist (T^[n + i] v₀) (T^[n + i + 1] v₀) := byX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝv₀:X →ᵇ ℝn:ℕk:ℕih:dist (T^[n] v₀) (T^[n + k] v₀) ≤ ∑ i ∈ Finset.range k, dist (T^[n + i] v₀) (T^[n + i + 1] v₀)⊢ ∑ i ∈ Finset.range k, dist (T^[n + i] v₀) (T^[n + i + 1] v₀) + dist (T^[n + k] v₀) (T^[n + k + 1] v₀) =
  ∑ i ∈ Finset.range (k + 1), dist (T^[n + i] v₀) (T^[n + i + 1] v₀)
          rw [Finset.sum_range_succ]All goals completed! 🐙

Lemma: Bound Arbitrary Difference Compact

∀ n, k ∈ ℕ, ∀ v ∈ B(X),\ ∑_{i = 1}^k d(T^{n + i - 1} v, T^{n + i} v) ≤ d(v, T v) \frac{β^n}{1 - β}. Proof.
First, apply Lemma: Bound Difference One, to each term in the sum to obtain ∑_{i = 1}^k d(T^{n + i - 1} v, T^{n + i} v) ≤ ∑_{i = 1}^k β^n d(v, Tv). Then, we can collect terms of the geometric sum to obtain the desired result by transitivity. ∑_{i = 1}^k β^n d(v, Tv) = \frac{β^n}{1 - β} d(v, Tv). ■

omit [Nonempty X] in
lemma bound_difference_arbitrary_compact {T : BoundedContinuousFunction X ℝ → BoundedContinuousFunction X ℝ} (v₀ : BoundedContinuousFunction X ℝ) (hT : IsContraction T): ∀ (n : ℕ) (k : ℕ), ∑ i ∈ Finset.range k, dist (T^[n + i] v₀) (T^[n + i + 1] v₀) ≤ dist v₀ (T v₀) * hT.β^n / (1 - hT.β):= byX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝv₀:X →ᵇ ℝhT:IsContraction T⊢ ∀ (n k : ℕ), ∑ i ∈ Finset.range k, dist (T^[n + i] v₀) (T^[n + i + 1] v₀) ≤ dist v₀ (T v₀) * hT.β ^ n / (1 - hT.β)
  -- Add weak inequalities for β from strict inequalities
  have hβ_ge0 : 0 ≤ hT.β := le_of_lt hT.hβ_gt0X:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝv₀:X →ᵇ ℝhT:IsContraction Thβ_ge0:0 ≤ hT.β⊢ ∀ (n k : ℕ), ∑ i ∈ Finset.range k, dist (T^[n + i] v₀) (T^[n + i + 1] v₀) ≤ dist v₀ (T v₀) * hT.β ^ n / (1 - hT.β)
  have hβ_le1 : hT.β ≤ 1 := le_of_lt hT.hβ_lt1X:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝv₀:X →ᵇ ℝhT:IsContraction Thβ_ge0:0 ≤ hT.βhβ_le1:hT.β ≤ 1⊢ ∀ (n k : ℕ), ∑ i ∈ Finset.range k, dist (T^[n + i] v₀) (T^[n + i + 1] v₀) ≤ dist v₀ (T v₀) * hT.β ^ n / (1 - hT.β)
  intro n kX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝv₀:X →ᵇ ℝhT:IsContraction Thβ_ge0:0 ≤ hT.βhβ_le1:hT.β ≤ 1n:ℕk:ℕ⊢ ∑ i ∈ Finset.range k, dist (T^[n + i] v₀) (T^[n + i + 1] v₀) ≤ dist v₀ (T v₀) * hT.β ^ n / (1 - hT.β)
  -- Chain comparisons to obtain the desired result by transitivity among them
  calc
    ∑ i ∈ Finset.range k, dist (T^[n + i] v₀) (T^[n + i + 1] v₀)
    _ ≤ ∑ i ∈ Finset.range k, hT.β^(n + i) * dist v₀ (T v₀) := byX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝv₀:X →ᵇ ℝhT:IsContraction Thβ_ge0:0 ≤ hT.βhβ_le1:hT.β ≤ 1n:ℕk:ℕ⊢ ∑ i ∈ Finset.range k, dist (T^[n + i] v₀) (T^[n + i + 1] v₀) ≤ ∑ i ∈ Finset.range k, hT.β ^ (n + i) * dist v₀ (T v₀)
      apply Finset.sum_le_sumhX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝv₀:X →ᵇ ℝhT:IsContraction Thβ_ge0:0 ≤ hT.βhβ_le1:hT.β ≤ 1n:ℕk:ℕ⊢ ∀ i ∈ Finset.range k, dist (T^[n + i] v₀) (T^[n + i + 1] v₀) ≤ hT.β ^ (n + i) * dist v₀ (T v₀)  -- Prove the sum inequality by proving the inequality for each component of the sum
      intro i _hihX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝv₀:X →ᵇ ℝhT:IsContraction Thβ_ge0:0 ≤ hT.βhβ_le1:hT.β ≤ 1n:ℕk:ℕi:ℕ_hi:i ∈ Finset.range k⊢ dist (T^[n + i] v₀) (T^[n + i + 1] v₀) ≤ hT.β ^ (n + i) * dist v₀ (T v₀)
      -- Apply the contraction result
      exact bound_difference_one v₀ hT (n + i)All goals completed! 🐙
    _ = ∑ i ∈ Finset.range k, (hT.β^n * dist v₀ (T v₀)) * hT.β^i := byX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝv₀:X →ᵇ ℝhT:IsContraction Thβ_ge0:0 ≤ hT.βhβ_le1:hT.β ≤ 1n:ℕk:ℕ⊢ ∑ i ∈ Finset.range k, hT.β ^ (n + i) * dist v₀ (T v₀) = ∑ i ∈ Finset.range k, hT.β ^ n * dist v₀ (T v₀) * hT.β ^ i
      -- Prove the two sums are equal by stating each element is equal (`rfl` already proves the indices are the same)
      apply Finset.sum_congr rflX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝv₀:X →ᵇ ℝhT:IsContraction Thβ_ge0:0 ≤ hT.βhβ_le1:hT.β ≤ 1n:ℕk:ℕ⊢ ∀ x ∈ Finset.range k, hT.β ^ (n + x) * dist v₀ (T v₀) = hT.β ^ n * dist v₀ (T v₀) * hT.β ^ x
      intro i _hiX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝv₀:X →ᵇ ℝhT:IsContraction Thβ_ge0:0 ≤ hT.βhβ_le1:hT.β ≤ 1n:ℕk:ℕi:ℕ_hi:i ∈ Finset.range k⊢ hT.β ^ (n + i) * dist v₀ (T v₀) = hT.β ^ n * dist v₀ (T v₀) * hT.β ^ i
      rw [pow_add]X:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝv₀:X →ᵇ ℝhT:IsContraction Thβ_ge0:0 ≤ hT.βhβ_le1:hT.β ≤ 1n:ℕk:ℕi:ℕ_hi:i ∈ Finset.range k⊢ hT.β ^ n * hT.β ^ i * dist v₀ (T v₀) = hT.β ^ n * dist v₀ (T v₀) * hT.β ^ i
      ringAll goals completed! 🐙
    _ = (hT.β^n * dist v₀ (T v₀)) * ∑ i ∈ Finset.range k, hT.β^i := byX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝv₀:X →ᵇ ℝhT:IsContraction Thβ_ge0:0 ≤ hT.βhβ_le1:hT.β ≤ 1n:ℕk:ℕ⊢ ∑ i ∈ Finset.range k, hT.β ^ n * dist v₀ (T v₀) * hT.β ^ i = hT.β ^ n * dist v₀ (T v₀) * ∑ i ∈ Finset.range k, hT.β ^ i
      rw [← Finset.mul_sum]All goals completed! 🐙
    _ ≤ (hT.β^n * dist v₀ (T v₀)) * (1 / (1 - hT.β)) := byX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝv₀:X →ᵇ ℝhT:IsContraction Thβ_ge0:0 ≤ hT.βhβ_le1:hT.β ≤ 1n:ℕk:ℕ⊢ hT.β ^ n * dist v₀ (T v₀) * ∑ i ∈ Finset.range k, hT.β ^ i ≤ hT.β ^ n * dist v₀ (T v₀) * (1 / (1 - hT.β))
      -- Rewrite as geometric sum, providing a proof that $`β ≠ 1` using $`β < 1`
      rw [geom_sum_eq (ne_of_lt hT.hβ_lt1)]X:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝv₀:X →ᵇ ℝhT:IsContraction Thβ_ge0:0 ≤ hT.βhβ_le1:hT.β ≤ 1n:ℕk:ℕ⊢ hT.β ^ n * dist v₀ (T v₀) * ((hT.β ^ k - 1) / (hT.β - 1)) ≤ hT.β ^ n * dist v₀ (T v₀) * (1 / (1 - hT.β))
      -- Flip (β^k - 1) / (β - 1) into (1 - β^k) / (1 - β)
      rw [← neg_sub 1 (hT.β^k), ← neg_sub 1 hT.β, neg_div_neg_eq]X:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝv₀:X →ᵇ ℝhT:IsContraction Thβ_ge0:0 ≤ hT.βhβ_le1:hT.β ≤ 1n:ℕk:ℕ⊢ hT.β ^ n * dist v₀ (T v₀) * ((1 - hT.β ^ k) / (1 - hT.β)) ≤ hT.β ^ n * dist v₀ (T v₀) * (1 / (1 - hT.β))
      gcongrhbc.hcX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝv₀:X →ᵇ ℝhT:IsContraction Thβ_ge0:0 ≤ hT.βhβ_le1:hT.β ≤ 1n:ℕk:ℕ⊢ 0 ≤ 1 - hT.βhbc.habX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝv₀:X →ᵇ ℝhT:IsContraction Thβ_ge0:0 ≤ hT.βhβ_le1:hT.β ≤ 1n:ℕk:ℕ⊢ 1 - hT.β ^ k ≤ 1
      -- First, prove that 0 ≤ 1 - β
      -- by applying the `sub_pos` tactic where we take the if direction. `.mp` is for the "if" direction of the logical equality
      exact sub_nonneg.mpr hβ_le1hbc.habX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝv₀:X →ᵇ ℝhT:IsContraction Thβ_ge0:0 ≤ hT.βhβ_le1:hT.β ≤ 1n:ℕk:ℕ⊢ 1 - hT.β ^ k ≤ 1
      -- Second, prove that 1 - β^k ≤ 1
      exact sub_le_self 1 (pow_nonneg hβ_ge0 k)All goals completed! 🐙
    _ = dist v₀ (T v₀) * hT.β^n / (1 - hT.β) := byX:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝv₀:X →ᵇ ℝhT:IsContraction Thβ_ge0:0 ≤ hT.βhβ_le1:hT.β ≤ 1n:ℕk:ℕ⊢ hT.β ^ n * dist v₀ (T v₀) * (1 / (1 - hT.β)) = dist v₀ (T v₀) * hT.β ^ n / (1 - hT.β)
      simp_rw [X:Type u_1inst✝:TopologicalSpace XT:(X →ᵇ ℝ) → X →ᵇ ℝv₀:X →ᵇ ℝhT:IsContraction Thβ_ge0:0 ≤ hT.βhβ_le1:hT.β ≤ 1n:ℕk:ℕ⊢ hT.β ^ n * dist v₀ (T v₀) * (1 / (1 - hT.β)) = dist v₀ (T v₀) * hT.β ^ n / (1 - hT.β)div_eq_inv_mul, mul_one]
      ringAll goals completed! 🐙