Theorem: iter_error_peel (Ray/Dynamics/Multibrot/Iterates.lean)

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ iter_error d c z = f_error d z + iter_error d c (f' d c z)
Tactic:
have h0 := sum_drop (iter_error_summable d z3 cz).hasSum
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
h0 :
  HasSum (fun n => f_error d ((f' d c)^[n + 1] z)) (∑' (b : ℕ), f_error d ((f' d c)^[b] z) - f_error d ((f' d c)^[0] z))
⊢ iter_error d c z = f_error d z + iter_error d c (f' d c z)

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
h0 :
  HasSum (fun n => f_error d ((f' d c)^[n + 1] z)) (∑' (b : ℕ), f_error d ((f' d c)^[b] z) - f_error d ((f' d c)^[0] z))
⊢ iter_error d c z = f_error d z + iter_error d c (f' d c z)
Tactic:
simp only [Function.iterate_succ_apply, zero_add, Function.iterate_zero, id_eq] at h0
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
h0 : HasSum (fun n => f_error d ((f' d c)^[n] (f' d c z))) (∑' (b : ℕ), f_error d ((f' d c)^[b] z) - f_error d z)
⊢ iter_error d c z = f_error d z + iter_error d c (f' d c z)

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
h0 : HasSum (fun n => f_error d ((f' d c)^[n] (f' d c z))) (∑' (b : ℕ), f_error d ((f' d c)^[b] z) - f_error d z)
⊢ iter_error d c z = f_error d z + iter_error d c (f' d c z)
Tactic:
simp only [iter_error, h0.tsum_eq]
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
h0 : HasSum (fun n => f_error d ((f' d c)^[n] (f' d c z))) (∑' (b : ℕ), f_error d ((f' d c)^[b] z) - f_error d z)
⊢ ∑' (n : ℕ), f_error d ((f' d c)^[n] z) = f_error d z + (∑' (n : ℕ), f_error d ((f' d c)^[n] z) - f_error d z)

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
h0 : HasSum (fun n => f_error d ((f' d c)^[n] (f' d c z))) (∑' (b : ℕ), f_error d ((f' d c)^[b] z) - f_error d z)
⊢ ∑' (n : ℕ), f_error d ((f' d c)^[n] z) = f_error d z + (∑' (n : ℕ), f_error d ((f' d c)^[n] z) - f_error d z)
Tactic:
abel
State after:
no goals