theorem
proved
tactic proof
defectIterate_succ
show as:
view Lean formalization →
formal statement (Lean)
89theorem defectIterate_succ (t : ℝ) (n : ℕ) :
90 defectIterate t (n + 1) = 2 * defectIterate t n * (defectIterate t n + 2) := by
proof body
Tactic-mode proof.
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ₙ. -/