Theorem: iter_small (Ray/Dynamics/Multibrot/Basic.lean)

State before:
c✝ : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
c z : ℂ
⊢ Complex.abs (f' d c z) ≤ Complex.abs z ^ d + Complex.abs c
Tactic:
calc abs (z^d + c)
  _ ≤ abs (z^d) + abs c := by bound
  _ ≤ abs z ^ d + abs c := by rw [Complex.abs.map_pow]
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
c z : ℂ
⊢ Complex.abs (z ^ d + c) ≤ Complex.abs (z ^ d) + Complex.abs c
Tactic:
bound
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
c z : ℂ
⊢ Complex.abs (z ^ d) + Complex.abs c ≤ Complex.abs z ^ d + Complex.abs c
Tactic:
rw [Complex.abs.map_pow]
State after:
no goals