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

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z6 : 6 ≤ Complex.abs z
⊢ f_error d z ≤ 0.565 / (Complex.abs z * (Complex.abs z).log)
Tactic:
refine f_error_le_generic d (b := 6) (l := 1.791) (s := 1.1) (t := 0.0512) (c := 1.027)
  (g := _) z6 (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 : ℂ
z6 : 6 ≤ Complex.abs z
⊢ exp 1.791 ≤ 6

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z6 : 6 ≤ Complex.abs z
⊢ exp 1.791 ≤ 6
Tactic:
norm_num
State after:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z6 : 6 ≤ Complex.abs z
⊢ (1791 / 1000).exp ≤ 6

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z6 : 6 ≤ Complex.abs z
⊢ (1791 / 1000).exp ≤ 6
Tactic:
exact (exp_div_lt).le
State after:
no goals

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

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z6 : 6 ≤ Complex.abs z
⊢ 1.1 / 6 / (2 * 1.791) ≤ 512e-4
Tactic:
norm_num
State after:
no goals

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

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

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z6 : 6 ≤ Complex.abs z
⊢ 1 / 2 * 1.027 * 1.1 ≤ 0.565
Tactic:
norm_num
State after:
no goals

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

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