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

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z33 : 33 ≤ Complex.abs z
⊢ f_error d z ≤ 0.512 / (Complex.abs z * (Complex.abs z).log)
Tactic:
refine f_error_le_generic d (b := 33) (l := 3.49) (s := 1.02) (t := 0.0045) (c := 1.003)
  (g := _) z33 (lb := ?_) (b3 := by norm_num) (st := by norm_num) (tc := by norm_num)
  (bs := by norm_num) (csg := by norm_num) (l0 := by norm_num) (c1 := by norm_num)
State after:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z33 : 33 ≤ Complex.abs z
⊢ exp 3.49 ≤ 33

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z33 : 33 ≤ Complex.abs z
⊢ exp 3.49 ≤ 33
Tactic:
norm_num
State after:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z33 : 33 ≤ Complex.abs z
⊢ (349 / 100).exp ≤ 33

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z33 : 33 ≤ Complex.abs z
⊢ (349 / 100).exp ≤ 33
Tactic:
exact (exp_div_lt).le
State after:
no goals

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z33 : 33 ≤ 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)
z : ℂ
z33 : 33 ≤ Complex.abs z
⊢ 1.02 / 33 / (2 * 3.49) ≤ 45e-4
Tactic:
norm_num
State after:
no goals

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z33 : 33 ≤ Complex.abs z
⊢ 45e-4 ≤ min 1 (((1.003 - 1) * 2)⁻¹ + 1)⁻¹
Tactic:
norm_num
State after:
no goals

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z33 : 33 ≤ Complex.abs z
⊢ 33⁻¹ ≤ min 1 (((1.02 - 1) * 2)⁻¹ + 1)⁻¹
Tactic:
norm_num
State after:
no goals

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

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

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