Theorem: log_neg_log_potential_approx (Ray/Dynamics/Multibrot/Potential.lean)

State before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ |(-(⋯.potential c ↑z).log).log - (Complex.abs z).log.log| ≤ iter_error d c z
Tactic:
apply le_of_forall_pos_lt_add
State after:
case h
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ ∀ (ε : ℝ), 0 < ε → |(-(⋯.potential c ↑z).log).log - (Complex.abs z).log.log| < iter_error d c z + ε

State before:
case h
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ ∀ (ε : ℝ), 0 < ε → |(-(⋯.potential c ↑z).log).log - (Complex.abs z).log.log| < iter_error d c z + ε
Tactic:
intro e ep
State after:
case h
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
e : ℝ
ep : 0 < e
⊢ |(-(⋯.potential c ↑z).log).log - (Complex.abs z).log.log| < iter_error d c z + e

State before:
case h
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
e : ℝ
ep : 0 < e
⊢ |(-(⋯.potential c ↑z).log).log - (Complex.abs z).log.log| < iter_error d c z + e
Tactic:
rcases (Metric.tendsto_nhds.mp (tendsto_log_neg_log_potential d z3 cz) e ep).exists with ⟨n,t⟩
State after:
case h.intro
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
e : ℝ
ep : 0 < e
n : ℕ
t : dist ((Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) (-(⋯.potential c ↑z).log).log < e
⊢ |(-(⋯.potential c ↑z).log).log - (Complex.abs z).log.log| < iter_error d c z + e

State before:
case h.intro
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
e : ℝ
ep : 0 < e
n : ℕ
t : dist ((Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) (-(⋯.potential c ↑z).log).log < e
⊢ |(-(⋯.potential c ↑z).log).log - (Complex.abs z).log.log| < iter_error d c z + e
Tactic:
have ie := iter_approx d z3 cz n
State after:
case h.intro
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
e : ℝ
ep : 0 < e
n : ℕ
t : dist ((Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) (-(⋯.potential c ↑z).log).log < e
ie : |(Complex.abs ((f' d c)^[n] z)).log.log - (Complex.abs z).log.log - ↑n * (↑d).log| ≤ iter_error d c z
⊢ |(-(⋯.potential c ↑z).log).log - (Complex.abs z).log.log| < iter_error d c z + e

State before:
case h.intro
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
e : ℝ
ep : 0 < e
n : ℕ
t : dist ((Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) (-(⋯.potential c ↑z).log).log < e
ie : |(Complex.abs ((f' d c)^[n] z)).log.log - (Complex.abs z).log.log - ↑n * (↑d).log| ≤ iter_error d c z
⊢ |(-(⋯.potential c ↑z).log).log - (Complex.abs z).log.log| < iter_error d c z + e
Tactic:
generalize log (-log ((superF d).potential c z)) = p at ie t
State after:
case h.intro
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
e : ℝ
ep : 0 < e
n : ℕ
ie : |(Complex.abs ((f' d c)^[n] z)).log.log - (Complex.abs z).log.log - ↑n * (↑d).log| ≤ iter_error d c z
p : ℝ
t : dist ((Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) p < e
⊢ |p - (Complex.abs z).log.log| < iter_error d c z + e

State before:
case h.intro
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
e : ℝ
ep : 0 < e
n : ℕ
ie : |(Complex.abs ((f' d c)^[n] z)).log.log - (Complex.abs z).log.log - ↑n * (↑d).log| ≤ iter_error d c z
p : ℝ
t : dist ((Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) p < e
⊢ |p - (Complex.abs z).log.log| < iter_error d c z + e
Tactic:
generalize log (log (Complex.abs ((f' d c)^[n] z))) = x at ie t
State after:
case h.intro
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
e : ℝ
ep : 0 < e
n : ℕ
p x : ℝ
ie : |x - (Complex.abs z).log.log - ↑n * (↑d).log| ≤ iter_error d c z
t : dist (x - ↑n * (↑d).log) p < e
⊢ |p - (Complex.abs z).log.log| < iter_error d c z + e

State before:
case h.intro
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
e : ℝ
ep : 0 < e
n : ℕ
p x : ℝ
ie : |x - (Complex.abs z).log.log - ↑n * (↑d).log| ≤ iter_error d c z
t : dist (x - ↑n * (↑d).log) p < e
⊢ |p - (Complex.abs z).log.log| < iter_error d c z + e
Tactic:
generalize log (log (Complex.abs z)) = y at ie t
State after:
case h.intro
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
e : ℝ
ep : 0 < e
n : ℕ
p x : ℝ
t : dist (x - ↑n * (↑d).log) p < e
y : ℝ
ie : |x - y - ↑n * (↑d).log| ≤ iter_error d c z
⊢ |p - y| < iter_error d c z + e

State before:
case h.intro
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
e : ℝ
ep : 0 < e
n : ℕ
p x : ℝ
t : dist (x - ↑n * (↑d).log) p < e
y : ℝ
ie : |x - y - ↑n * (↑d).log| ≤ iter_error d c z
⊢ |p - y| < iter_error d c z + e
Tactic:
rw [Real.dist_eq, abs_sub_comm] at t
State after:
case h.intro
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
e : ℝ
ep : 0 < e
n : ℕ
p x : ℝ
t : |p - (x - ↑n * (↑d).log)| < e
y : ℝ
ie : |x - y - ↑n * (↑d).log| ≤ iter_error d c z
⊢ |p - y| < iter_error d c z + e

State before:
case h.intro
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
e : ℝ
ep : 0 < e
n : ℕ
p x : ℝ
t : |p - (x - ↑n * (↑d).log)| < e
y : ℝ
ie : |x - y - ↑n * (↑d).log| ≤ iter_error d c z
⊢ |p - y| < iter_error d c z + e
Tactic:
rw [add_comm]
State after:
case h.intro
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
e : ℝ
ep : 0 < e
n : ℕ
p x : ℝ
t : |p - (x - ↑n * (↑d).log)| < e
y : ℝ
ie : |x - y - ↑n * (↑d).log| ≤ iter_error d c z
⊢ |p - y| < e + iter_error d c z

State before:
case h.intro
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
e : ℝ
ep : 0 < e
n : ℕ
p x : ℝ
t : |p - (x - ↑n * (↑d).log)| < e
y : ℝ
ie : |x - y - ↑n * (↑d).log| ≤ iter_error d c z
⊢ |p - y| < e + iter_error d c z
Tactic:
calc |p - y|
    _ = |(p - (x - n * log d)) + (x - y - n * log d)| := by ring_nf
    _ ≤ |p - (x - n * log d)| + |x - y - n * log d| := abs_add _ _
    _ < e + _ := add_lt_add_of_lt_of_le t ie
State after:
no goals

State before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
e : ℝ
ep : 0 < e
n : ℕ
p x : ℝ
t : |p - (x - ↑n * (↑d).log)| < e
y : ℝ
ie : |x - y - ↑n * (↑d).log| ≤ iter_error d c z
⊢ |p - y| = |p - (x - ↑n * (↑d).log) + (x - y - ↑n * (↑d).log)|
Tactic:
ring_nf
State after:
no goals