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

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z12 : 12 ≤ Complex.abs z
⊢ f_error d z ≤ 0.528 / (Complex.abs z * (Complex.abs z).log)
Tactic:
refine f_error_le_generic d (b := 12) (l := 2.48) (s := 1.046) (t := 0.0176) (c := 1.009)
  (g := _) z12 (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 : ℂ
z12 : 12 ≤ Complex.abs z
⊢ exp 2.48 ≤ 12

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z12 : 12 ≤ Complex.abs z
⊢ exp 2.48 ≤ 12
Tactic:
norm_num
State after:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z12 : 12 ≤ Complex.abs z
⊢ (62 / 25).exp ≤ 12

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z12 : 12 ≤ Complex.abs z
⊢ (62 / 25).exp ≤ 12
Tactic:
exact (exp_div_lt).le
State after:
no goals

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

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z12 : 12 ≤ Complex.abs z
⊢ 1.046 / 12 / (2 * 2.48) ≤ 176e-4
Tactic:
norm_num
State after:
no goals

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

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

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z12 : 12 ≤ Complex.abs z
⊢ 1 / 2 * 1.009 * 1.046 ≤ 0.528
Tactic:
norm_num
State after:
no goals

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

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