contraction_converges

formal source

  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
  58    have h_denom : 0 < 2 * x := by positivity
  59    have h_sq : (x - 1) ^ 2 = 0 := by
  60      by_contra hne
  61      have hpos : 0 < (x - 1) ^ 2 := lt_of_le_of_ne (sq_nonneg _) (Ne.symm hne)
  62      have : 0 < (x - 1) ^ 2 / (2 * x) := div_pos hpos h_denom
  63      linarith
  64    have : x - 1 = 0 := by
  65      rcases sq_eq_zero_iff.mp h_sq with h