defectIterate_succ

formal source

  86      cosh(2·u) = 2cosh²(u) − 1
  87      ⟹ cosh(2u)−1 = 2(cosh u − 1)(cosh u + 1)
  88                    = 2·(cosh u − 1)·((cosh u − 1) + 2) -/
  89theorem defectIterate_succ (t : ℝ) (n : ℕ) :
  90    defectIterate t (n + 1) = 2 * defectIterate t n * (defectIterate t n + 2) := by
  91  simp only [defectIterate]
  92  rw [show (2 : ℝ) ^ (n + 1) * t = 2 * ((2 : ℝ) ^ n * t) from by rw [pow_succ]; ring]
  93  have hd := Real.cosh_two_mul ((2 : ℝ) ^ n * t)
  94  have hs := Real.cosh_sq ((2 : ℝ) ^ n * t)
  95  set c := Real.cosh ((2 : ℝ) ^ n * t)
  96  set s := Real.sinh ((2 : ℝ) ^ n * t)
  97  have lhs : Real.cosh (2 * ((2 : ℝ) ^ n * t)) - 1 = 2 * c ^ 2 - 2 := by linarith
  98  have rhs_eq : 2 * (c - 1) * (c - 1 + 2) = 2 * c ^ 2 - 2 := by ring
  99  linarith
 100
 101/-- The recurrence in "squared ratio" form:
 102    dₙ₊₁ = 2(dₙ² + 2dₙ) = 2dₙ² + 4dₙ. -/
 103theorem defectIterate_succ' (t : ℝ) (n : ℕ) :
 104    defectIterate t (n + 1) = 2 * (defectIterate t n) ^ 2 + 4 * defectIterate t n := by
 105  rw [defectIterate_succ]; ring
 106
 107/-! ## §3. Defect amplification -/
 108
 109/-- **Each iteration at least quadruples the defect.**
 110    dₙ₊₁ ≥ 4·dₙ  (from dₙ ≥ 0 ⟹ dₙ+2 ≥ 2). -/
 111theorem defectIterate_four_mul_le (t : ℝ) (n : ℕ) :
 112    4 * defectIterate t n ≤ defectIterate t (n + 1) := by
 113  rw [defectIterate_succ]
 114  have hd : 0 ≤ defectIterate t n := defectIterate_nonneg t n
 115  nlinarith [sq_nonneg (defectIterate t n)]
 116
 117/-- **Exponential lower bound.** dₙ ≥ 4ⁿ · d₀.
 118
 119    Each iteration quadruples the defect, so after n iterations