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

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z140 : 140 ≤ Complex.abs z
⊢ f_error d z ≤ 0.5023 / (Complex.abs z * (Complex.abs z).log)
Tactic:
refine f_error_le_generic d (b := 140) (l := 4.94) (s := 1.004) (t := 0.00073) (c := 1.0004)
  (g := _) z140 (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 : ℂ
z140 : 140 ≤ Complex.abs z
⊢ exp 4.94 ≤ 140

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z140 : 140 ≤ Complex.abs z
⊢ exp 4.94 ≤ 140
Tactic:
norm_num
State after:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z140 : 140 ≤ Complex.abs z
⊢ (247 / 50).exp ≤ 140

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z140 : 140 ≤ Complex.abs z
⊢ (247 / 50).exp ≤ 140
Tactic:
exact (exp_div_lt).le
State after:
no goals

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

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z140 : 140 ≤ Complex.abs z
⊢ 1.004 / 140 / (2 * 4.94) ≤ 73e-5
Tactic:
norm_num
State after:
no goals

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z140 : 140 ≤ Complex.abs z
⊢ 73e-5 ≤ min 1 (((1.0004 - 1) * 2)⁻¹ + 1)⁻¹
Tactic:
norm_num
State after:
no goals

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

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z140 : 140 ≤ Complex.abs z
⊢ 1 / 2 * 1.0004 * 1.004 ≤ 0.5023
Tactic:
norm_num
State after:
no goals

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

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