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

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ iter_error d c z ≤ (Complex.abs z).log.log
Tactic:
have hl : 1.38 ≤ log (abs z) := by
  rw [Real.le_log_iff_exp_le (by positivity)]
  norm_num
  exact le_trans (exp_div_lt).le z4
State after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
hl : 1.38 ≤ (Complex.abs z).log
⊢ iter_error d c z ≤ (Complex.abs z).log.log

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
hl : 1.38 ≤ (Complex.abs z).log
⊢ iter_error d c z ≤ (Complex.abs z).log.log
Tactic:
have hll : 0.32 ≤ log (log (abs z)) := by
  rw [Real.le_log_iff_exp_le (by positivity)]
  norm_num
  exact le_trans (exp_div_lt).le hl
State after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
hl : 1.38 ≤ (Complex.abs z).log
hll : 0.32 ≤ (Complex.abs z).log.log
⊢ iter_error d c z ≤ (Complex.abs z).log.log

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
hl : 1.38 ≤ (Complex.abs z).log
hll : 0.32 ≤ (Complex.abs z).log.log
⊢ iter_error d c z ≤ (Complex.abs z).log.log
Tactic:
refine le_trans ?_ hll
State after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
hl : 1.38 ≤ (Complex.abs z).log
hll : 0.32 ≤ (Complex.abs z).log.log
⊢ iter_error d c z ≤ 0.32

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
hl : 1.38 ≤ (Complex.abs z).log
hll : 0.32 ≤ (Complex.abs z).log.log
⊢ iter_error d c z ≤ 0.32
Tactic:
apply le_trans (iter_error_le_of_z4 d z4 cz)
State after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
hl : 1.38 ≤ (Complex.abs z).log
hll : 0.32 ≤ (Complex.abs z).log.log
⊢ 0.8095 / (Complex.abs z * (Complex.abs z).log) ≤ 0.32

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
hl : 1.38 ≤ (Complex.abs z).log
hll : 0.32 ≤ (Complex.abs z).log.log
⊢ 0.8095 / (Complex.abs z * (Complex.abs z).log) ≤ 0.32
Tactic:
rw [div_le_iff' (by positivity), ←div_le_iff (by norm_num)]
State after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
hl : 1.38 ≤ (Complex.abs z).log
hll : 0.32 ≤ (Complex.abs z).log.log
⊢ 0.8095 / 0.32 ≤ Complex.abs z * (Complex.abs z).log

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
hl : 1.38 ≤ (Complex.abs z).log
hll : 0.32 ≤ (Complex.abs z).log.log
⊢ 0.8095 / 0.32 ≤ Complex.abs z * (Complex.abs z).log
Tactic:
refine le_trans (by norm_num) (mul_le_mul z4 hl (by positivity) (by positivity))
State after:
no goals

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 1.38 ≤ (Complex.abs z).log
Tactic:
rw [Real.le_log_iff_exp_le (by positivity)]
State after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ exp 1.38 ≤ Complex.abs z

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ exp 1.38 ≤ Complex.abs z
Tactic:
norm_num
State after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ (69 / 50).exp ≤ Complex.abs z

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ (69 / 50).exp ≤ Complex.abs z
Tactic:
exact le_trans (exp_div_lt).le z4
State after:
no goals

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

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
hl : 1.38 ≤ (Complex.abs z).log
⊢ 0.32 ≤ (Complex.abs z).log.log
Tactic:
rw [Real.le_log_iff_exp_le (by positivity)]
State after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
hl : 1.38 ≤ (Complex.abs z).log
⊢ exp 0.32 ≤ (Complex.abs z).log

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
hl : 1.38 ≤ (Complex.abs z).log
⊢ exp 0.32 ≤ (Complex.abs z).log
Tactic:
norm_num
State after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
hl : 1.38 ≤ (Complex.abs z).log
⊢ (8 / 25).exp ≤ (Complex.abs z).log

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
hl : 1.38 ≤ (Complex.abs z).log
⊢ (8 / 25).exp ≤ (Complex.abs z).log
Tactic:
exact le_trans (exp_div_lt).le hl
State after:
no goals

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
hl : 1.38 ≤ (Complex.abs z).log
⊢ 0 < (Complex.abs z).log
Tactic:
positivity
State after:
no goals

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
hl : 1.38 ≤ (Complex.abs z).log
hll : 0.32 ≤ (Complex.abs z).log.log
⊢ 0 < Complex.abs z * (Complex.abs z).log
Tactic:
positivity
State after:
no goals

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
hl : 1.38 ≤ (Complex.abs z).log
hll : 0.32 ≤ (Complex.abs z).log.log
⊢ 0 < 0.32
Tactic:
norm_num
State after:
no goals

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
hl : 1.38 ≤ (Complex.abs z).log
hll : 0.32 ≤ (Complex.abs z).log.log
⊢ 0.8095 / 0.32 ≤ 4 * 1.38
Tactic:
norm_num
State after:
no goals

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
hl : 1.38 ≤ (Complex.abs z).log
hll : 0.32 ≤ (Complex.abs z).log.log
⊢ 0 ≤ 1.38
Tactic:
positivity
State after:
no goals

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
hl : 1.38 ≤ (Complex.abs z).log
hll : 0.32 ≤ (Complex.abs z).log.log
⊢ 0 ≤ Complex.abs z
Tactic:
positivity
State after:
no goals