Contraction

formal source

  24open Cost
  25
  26/-- A contraction on a finite lattice: J-cost strictly decreases per step. -/
  27structure Contraction where
  28  step : ℝ → ℝ
  29  contraction_rate : ℝ
  30  rate_pos : 0 < contraction_rate
  31  rate_lt_one : contraction_rate < 1
  32  contracts : ∀ x, 0 < x → |step x - 1| ≤ contraction_rate * |x - 1|
  33
  34/-- Iterated contraction converges: for n >= 1, the error shrinks. -/
  35theorem contraction_converges (c : Contraction) (x₀ : ℝ) (hx : 0 < x₀) (n : ℕ)
  36    (hn : 0 < n) :
  37    c.contraction_rate ^ n * |x₀ - 1| < |x₀ - 1| ∨ x₀ = 1 := by
  38  by_cases h : x₀ = 1
  39  · right; exact h
  40  · left
  41    have hne : |x₀ - 1| > 0 := abs_pos.mpr (sub_ne_zero.mpr h)
  42    have : c.contraction_rate ^ n < 1 := by
  43      calc c.contraction_rate ^ n
  44          ≤ c.contraction_rate ^ 1 := by
  45            apply pow_le_pow_of_le_one (le_of_lt c.rate_pos) (le_of_lt c.rate_lt_one)
  46            exact hn
  47        _ = c.contraction_rate := pow_one _
  48        _ < 1 := c.rate_lt_one
  49    exact mul_lt_of_lt_one_left hne this
  50
  51/-- The global J-cost minimum is unique: x = 1 (defect = 0). -/
  52theorem global_minimum_unique (x : ℝ) (hx : 0 < x) :
  53    Jcost x = 0 ↔ x = 1 := by
  54  constructor
  55  · intro h
  56    have hx0 : x ≠ 0 := ne_of_gt hx
  57    rw [Jcost_eq_sq hx0] at h