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

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
⊢ |(Complex.abs ((f' d c)^[n] z)).log.log - (Complex.abs z).log.log - ↑n * (↑d).log| ≤ iter_error d c z
Tactic:
induction' n with n h generalizing z
State after:
case zero
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ |(Complex.abs ((f' d c)^[0] z)).log.log - (Complex.abs z).log.log - ↑0 * (↑d).log| ≤ iter_error d c z

case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
n : ℕ
h :
  ∀ {z : ℂ},
    3 ≤ Complex.abs z →
      Complex.abs c ≤ Complex.abs z →
        |(Complex.abs ((f' d c)^[n] z)).log.log - (Complex.abs z).log.log - ↑n * (↑d).log| ≤ iter_error d c z
z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ |(Complex.abs ((f' d c)^[n + 1] z)).log.log - (Complex.abs z).log.log - ↑(n + 1) * (↑d).log| ≤ iter_error d c z

State before:
case zero
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ |(Complex.abs ((f' d c)^[0] z)).log.log - (Complex.abs z).log.log - ↑0 * (↑d).log| ≤ iter_error d c z
Tactic:
simp only [Nat.zero_eq, Function.iterate_zero, id_eq, sub_self, CharP.cast_eq_zero, zero_mul,
  abs_zero, iter_error_nonneg d z3 cz]
State after:
no goals

State before:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
n : ℕ
h :
  ∀ {z : ℂ},
    3 ≤ Complex.abs z →
      Complex.abs c ≤ Complex.abs z →
        |(Complex.abs ((f' d c)^[n] z)).log.log - (Complex.abs z).log.log - ↑n * (↑d).log| ≤ iter_error d c z
z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ |(Complex.abs ((f' d c)^[n + 1] z)).log.log - (Complex.abs z).log.log - ↑(n + 1) * (↑d).log| ≤ iter_error d c z
Tactic:
simp only [Finset.sum_range_succ, Function.iterate_succ_apply, Nat.succ_eq_add_one,
  Nat.cast_add_one]
State after:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
n : ℕ
h :
  ∀ {z : ℂ},
    3 ≤ Complex.abs z →
      Complex.abs c ≤ Complex.abs z →
        |(Complex.abs ((f' d c)^[n] z)).log.log - (Complex.abs z).log.log - ↑n * (↑d).log| ≤ iter_error d c z
z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ |(Complex.abs ((f' d c)^[n] (f' d c z))).log.log - (Complex.abs z).log.log - (↑n + 1) * (↑d).log| ≤ iter_error d c z

State before:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
n : ℕ
h :
  ∀ {z : ℂ},
    3 ≤ Complex.abs z →
      Complex.abs c ≤ Complex.abs z →
        |(Complex.abs ((f' d c)^[n] z)).log.log - (Complex.abs z).log.log - ↑n * (↑d).log| ≤ iter_error d c z
z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ |(Complex.abs ((f' d c)^[n] (f' d c z))).log.log - (Complex.abs z).log.log - (↑n + 1) * (↑d).log| ≤ iter_error d c z
Tactic:
have e : log (log (abs ((f' d c)^[n] (f' d c z)))) - log (log (abs z)) - (n+1) * log d =
    (log (log (abs (f' d c z))) - log (log (abs z)) - log d) +
    (log (log (abs ((f' d c)^[n] (f' d c z)))) - log (log (abs (f' d c z))) - n * log d) := by
  ring
State after:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
n : ℕ
h :
  ∀ {z : ℂ},
    3 ≤ Complex.abs z →
      Complex.abs c ≤ Complex.abs z →
        |(Complex.abs ((f' d c)^[n] z)).log.log - (Complex.abs z).log.log - ↑n * (↑d).log| ≤ iter_error d c z
z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
e :
  (Complex.abs ((f' d c)^[n] (f' d c z))).log.log - (Complex.abs z).log.log - (↑n + 1) * (↑d).log =
    (Complex.abs (f' d c z)).log.log - (Complex.abs z).log.log - (↑d).log +
      ((Complex.abs ((f' d c)^[n] (f' d c z))).log.log - (Complex.abs (f' d c z)).log.log - ↑n * (↑d).log)
⊢ |(Complex.abs ((f' d c)^[n] (f' d c z))).log.log - (Complex.abs z).log.log - (↑n + 1) * (↑d).log| ≤ iter_error d c z

State before:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
n : ℕ
h :
  ∀ {z : ℂ},
    3 ≤ Complex.abs z →
      Complex.abs c ≤ Complex.abs z →
        |(Complex.abs ((f' d c)^[n] z)).log.log - (Complex.abs z).log.log - ↑n * (↑d).log| ≤ iter_error d c z
z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
e :
  (Complex.abs ((f' d c)^[n] (f' d c z))).log.log - (Complex.abs z).log.log - (↑n + 1) * (↑d).log =
    (Complex.abs (f' d c z)).log.log - (Complex.abs z).log.log - (↑d).log +
      ((Complex.abs ((f' d c)^[n] (f' d c z))).log.log - (Complex.abs (f' d c z)).log.log - ↑n * (↑d).log)
⊢ |(Complex.abs ((f' d c)^[n] (f' d c z))).log.log - (Complex.abs z).log.log - (↑n + 1) * (↑d).log| ≤ iter_error d c z
Tactic:
rw [e, iter_error_peel z3 cz]
State after:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
n : ℕ
h :
  ∀ {z : ℂ},
    3 ≤ Complex.abs z →
      Complex.abs c ≤ Complex.abs z →
        |(Complex.abs ((f' d c)^[n] z)).log.log - (Complex.abs z).log.log - ↑n * (↑d).log| ≤ iter_error d c z
z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
e :
  (Complex.abs ((f' d c)^[n] (f' d c z))).log.log - (Complex.abs z).log.log - (↑n + 1) * (↑d).log =
    (Complex.abs (f' d c z)).log.log - (Complex.abs z).log.log - (↑d).log +
      ((Complex.abs ((f' d c)^[n] (f' d c z))).log.log - (Complex.abs (f' d c z)).log.log - ↑n * (↑d).log)
⊢ |(Complex.abs (f' d c z)).log.log - (Complex.abs z).log.log - (↑d).log +
        ((Complex.abs ((f' d c)^[n] (f' d c z))).log.log - (Complex.abs (f' d c z)).log.log - ↑n * (↑d).log)| ≤
    f_error d z + iter_error d c (f' d c z)

State before:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
n : ℕ
h :
  ∀ {z : ℂ},
    3 ≤ Complex.abs z →
      Complex.abs c ≤ Complex.abs z →
        |(Complex.abs ((f' d c)^[n] z)).log.log - (Complex.abs z).log.log - ↑n * (↑d).log| ≤ iter_error d c z
z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
e :
  (Complex.abs ((f' d c)^[n] (f' d c z))).log.log - (Complex.abs z).log.log - (↑n + 1) * (↑d).log =
    (Complex.abs (f' d c z)).log.log - (Complex.abs z).log.log - (↑d).log +
      ((Complex.abs ((f' d c)^[n] (f' d c z))).log.log - (Complex.abs (f' d c z)).log.log - ↑n * (↑d).log)
⊢ |(Complex.abs (f' d c z)).log.log - (Complex.abs z).log.log - (↑d).log +
        ((Complex.abs ((f' d c)^[n] (f' d c z))).log.log - (Complex.abs (f' d c z)).log.log - ↑n * (↑d).log)| ≤
    f_error d z + iter_error d c (f' d c z)
Tactic:
have le : abs z ≤ abs (f' d c z) := le_self_iter d z3 cz 1
State after:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
n : ℕ
h :
  ∀ {z : ℂ},
    3 ≤ Complex.abs z →
      Complex.abs c ≤ Complex.abs z →
        |(Complex.abs ((f' d c)^[n] z)).log.log - (Complex.abs z).log.log - ↑n * (↑d).log| ≤ iter_error d c z
z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
e :
  (Complex.abs ((f' d c)^[n] (f' d c z))).log.log - (Complex.abs z).log.log - (↑n + 1) * (↑d).log =
    (Complex.abs (f' d c z)).log.log - (Complex.abs z).log.log - (↑d).log +
      ((Complex.abs ((f' d c)^[n] (f' d c z))).log.log - (Complex.abs (f' d c z)).log.log - ↑n * (↑d).log)
le : Complex.abs z ≤ Complex.abs (f' d c z)
⊢ |(Complex.abs (f' d c z)).log.log - (Complex.abs z).log.log - (↑d).log +
        ((Complex.abs ((f' d c)^[n] (f' d c z))).log.log - (Complex.abs (f' d c z)).log.log - ↑n * (↑d).log)| ≤
    f_error d z + iter_error d c (f' d c z)

State before:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
n : ℕ
h :
  ∀ {z : ℂ},
    3 ≤ Complex.abs z →
      Complex.abs c ≤ Complex.abs z →
        |(Complex.abs ((f' d c)^[n] z)).log.log - (Complex.abs z).log.log - ↑n * (↑d).log| ≤ iter_error d c z
z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
e :
  (Complex.abs ((f' d c)^[n] (f' d c z))).log.log - (Complex.abs z).log.log - (↑n + 1) * (↑d).log =
    (Complex.abs (f' d c z)).log.log - (Complex.abs z).log.log - (↑d).log +
      ((Complex.abs ((f' d c)^[n] (f' d c z))).log.log - (Complex.abs (f' d c z)).log.log - ↑n * (↑d).log)
le : Complex.abs z ≤ Complex.abs (f' d c z)
⊢ |(Complex.abs (f' d c z)).log.log - (Complex.abs z).log.log - (↑d).log +
        ((Complex.abs ((f' d c)^[n] (f' d c z))).log.log - (Complex.abs (f' d c z)).log.log - ↑n * (↑d).log)| ≤
    f_error d z + iter_error d c (f' d c z)
Tactic:
exact le_trans (abs_add _ _) (add_le_add (f_approx z3 cz)
  (h (le_trans z3 le) (le_trans cz le)))
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
n : ℕ
h :
  ∀ {z : ℂ},
    3 ≤ Complex.abs z →
      Complex.abs c ≤ Complex.abs z →
        |(Complex.abs ((f' d c)^[n] z)).log.log - (Complex.abs z).log.log - ↑n * (↑d).log| ≤ iter_error d c z
z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ (Complex.abs ((f' d c)^[n] (f' d c z))).log.log - (Complex.abs z).log.log - (↑n + 1) * (↑d).log =
    (Complex.abs (f' d c z)).log.log - (Complex.abs z).log.log - (↑d).log +
      ((Complex.abs ((f' d c)^[n] (f' d c z))).log.log - (Complex.abs (f' d c z)).log.log - ↑n * (↑d).log)
Tactic:
ring
State after:
no goals