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

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z33 : 33 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ iter_error d c z ≤ 0.529 / (Complex.abs z * (Complex.abs z).log)
Tactic:
refine le_trans (iter_error_weak d (b := 33) (by norm_num) (by norm_num)
  (fun {_} bz ↦ f_error_le_of_z33 d bz) z33 cz) ?_
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z33 : 33 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 0.512 / (1 - (33 - 1)⁻¹) / (Complex.abs z * (Complex.abs z).log) ≤ 0.529 / (Complex.abs z * (Complex.abs z).log)

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z33 : 33 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 0.512 / (1 - (33 - 1)⁻¹) / (Complex.abs z * (Complex.abs z).log) ≤ 0.529 / (Complex.abs z * (Complex.abs z).log)
Tactic:
have l0 : 0 < log (abs z) :=
  lt_of_lt_of_le (by norm_num) (le_log_abs_z (le_trans (by norm_num) z33))
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z33 : 33 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
l0 : 0 < (Complex.abs z).log
⊢ 0.512 / (1 - (33 - 1)⁻¹) / (Complex.abs z * (Complex.abs z).log) ≤ 0.529 / (Complex.abs z * (Complex.abs z).log)

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z33 : 33 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
l0 : 0 < (Complex.abs z).log
⊢ 0.512 / (1 - (33 - 1)⁻¹) / (Complex.abs z * (Complex.abs z).log) ≤ 0.529 / (Complex.abs z * (Complex.abs z).log)
Tactic:
exact div_le_div_of_nonneg_right (by norm_num) (by positivity)
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z33 : 33 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 3 ≤ 33
Tactic:
norm_num
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z33 : 33 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 0 ≤ 0.512
Tactic:
norm_num
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z33 : 33 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 0 < 1.0986
Tactic:
norm_num
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z33 : 33 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
l0 : 0 < (Complex.abs z).log
⊢ 0.512 / (1 - (33 - 1)⁻¹) ≤ 0.529
Tactic:
norm_num
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z33 : 33 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
l0 : 0 < (Complex.abs z).log
⊢ 0 ≤ Complex.abs z * (Complex.abs z).log
Tactic:
positivity
State after:
no goals