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

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
⊢ f_error d z ≤ 0.699 / (Complex.abs z * (Complex.abs z).log)
Tactic:
refine f_error_le_generic d 3 1.0986 (s := 1.25) (t := 0.1897) (c := 1.1171) _ z3 ?_
State after:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
⊢ exp 1.0986 ≤ 3

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
⊢ exp 1.0986 ≤ 3
Tactic:
norm_num
State after:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
⊢ (5493 / 5000).exp ≤ 3

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
⊢ (5493 / 5000).exp ≤ 3
Tactic:
exact (exp_div_lt).le
State after:
no goals