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

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z4 : 4 ≤ Complex.abs z
⊢ f_error d z ≤ 0.619 / (Complex.abs z * (Complex.abs z).log)
Tactic:
refine f_error_le_generic d (b := 4) (l := 1.3862) (s := 1.167) (t := 0.106) (c := 1.06)
  (g := _) z4 (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 : ℂ
z4 : 4 ≤ Complex.abs z
⊢ exp 1.3862 ≤ 4

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z4 : 4 ≤ Complex.abs z
⊢ exp 1.3862 ≤ 4
Tactic:
norm_num
State after:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z4 : 4 ≤ Complex.abs z
⊢ (6931 / 5000).exp ≤ 4

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

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

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z4 : 4 ≤ Complex.abs z
⊢ 1.167 / 4 / (2 * 1.3862) ≤ 0.106
Tactic:
norm_num
State after:
no goals

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

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

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z4 : 4 ≤ Complex.abs z
⊢ 1 / 2 * 1.06 * 1.167 ≤ 0.619
Tactic:
norm_num
State after:
no goals

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

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