internlm/Lean-Github huggingface dataset:
Theorem: f_error_le_generic
Proof state before:
case refine_2
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
inner_le : -(1 - 1 / Complex.abs z).log ≤ s / Complex.abs z
dm : 2 * (Complex.abs z).log ≤ ↑d * (Complex.abs z).log
div_le : -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) ≤ t
⊢ c * (-(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)) ≤ g / (Complex.abs z * (Complex.abs z).log)
Tactic:
refine le_trans (mul_le_mul_of_nonneg_left (div_le_div (by positivity) inner_le
  (by positivity) dm) (by positivity)) ?_
Proof state after:
case refine_2
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
inner_le : -(1 - 1 / Complex.abs z).log ≤ s / Complex.abs z
dm : 2 * (Complex.abs z).log ≤ ↑d * (Complex.abs z).log
div_le : -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) ≤ t
⊢ c * (s / Complex.abs z / (2 * (Complex.abs z).log)) ≤ g / (Complex.abs z * (Complex.abs z).log)
Theorem: f_error_le_generic
Proof state before:
case refine_2
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
inner_le : -(1 - 1 / Complex.abs z).log ≤ s / Complex.abs z
dm : 2 * (Complex.abs z).log ≤ ↑d * (Complex.abs z).log
div_le : -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) ≤ t
⊢ c * (s / Complex.abs z / (2 * (Complex.abs z).log)) ≤ g / (Complex.abs z * (Complex.abs z).log)
Tactic:
simp only [div_eq_mul_inv, ←mul_assoc, mul_inv, mul_comm _ (2⁻¹ : ℝ)]
Proof state after:
case refine_2
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
inner_le : -(1 - 1 / Complex.abs z).log ≤ s / Complex.abs z
dm : 2 * (Complex.abs z).log ≤ ↑d * (Complex.abs z).log
div_le : -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) ≤ t
⊢ 2⁻¹ * c * s * (Complex.abs z)⁻¹ * (Complex.abs z).log⁻¹ ≤ g * (Complex.abs z)⁻¹ * (Complex.abs z).log⁻¹
Theorem: f_error_le_generic
Proof state before:
case refine_2
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
inner_le : -(1 - 1 / Complex.abs z).log ≤ s / Complex.abs z
dm : 2 * (Complex.abs z).log ≤ ↑d * (Complex.abs z).log
div_le : -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) ≤ t
⊢ 2⁻¹ * c * s * (Complex.abs z)⁻¹ * (Complex.abs z).log⁻¹ ≤ g * (Complex.abs z)⁻¹ * (Complex.abs z).log⁻¹
Tactic:
norm_num
Proof state after:
case refine_2
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
inner_le : -(1 - 1 / Complex.abs z).log ≤ s / Complex.abs z
dm : 2 * (Complex.abs z).log ≤ ↑d * (Complex.abs z).log
div_le : -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) ≤ t
⊢ 1 / 2 * c * s * (Complex.abs z)⁻¹ * (Complex.abs z).log⁻¹ ≤ g * (Complex.abs z)⁻¹ * (Complex.abs z).log⁻¹
Theorem: f_error_le_generic
Proof state before:
case refine_2
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
inner_le : -(1 - 1 / Complex.abs z).log ≤ s / Complex.abs z
dm : 2 * (Complex.abs z).log ≤ ↑d * (Complex.abs z).log
div_le : -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) ≤ t
⊢ 1 / 2 * c * s * (Complex.abs z)⁻¹ * (Complex.abs z).log⁻¹ ≤ g * (Complex.abs z)⁻¹ * (Complex.abs z).log⁻¹
Tactic:
simp only [mul_assoc _ (abs z)⁻¹ _]
Proof state after:
case refine_2
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
inner_le : -(1 - 1 / Complex.abs z).log ≤ s / Complex.abs z
dm : 2 * (Complex.abs z).log ≤ ↑d * (Complex.abs z).log
div_le : -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) ≤ t
⊢ 1 / 2 * c * s * ((Complex.abs z)⁻¹ * (Complex.abs z).log⁻¹) ≤ g * ((Complex.abs z)⁻¹ * (Complex.abs z).log⁻¹)
Theorem: f_error_le_generic
Proof state before:
case refine_2
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
inner_le : -(1 - 1 / Complex.abs z).log ≤ s / Complex.abs z
dm : 2 * (Complex.abs z).log ≤ ↑d * (Complex.abs z).log
div_le : -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) ≤ t
⊢ 1 / 2 * c * s * ((Complex.abs z)⁻¹ * (Complex.abs z).log⁻¹) ≤ g * ((Complex.abs z)⁻¹ * (Complex.abs z).log⁻¹)
Tactic:
exact mul_le_mul_of_nonneg_right csg (by positivity)
Proof state after:
no goals
Theorem: f_error_le_generic
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
inner_le : -(1 - 1 / Complex.abs z).log ≤ s / Complex.abs z
dm : 2 * (Complex.abs z).log ≤ ↑d * (Complex.abs z).log
div_le : -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) ≤ t
⊢ 0 ≤ s / Complex.abs z
Tactic:
positivity
Proof state after:
no goals
Theorem: f_error_le_generic
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
inner_le : -(1 - 1 / Complex.abs z).log ≤ s / Complex.abs z
dm : 2 * (Complex.abs z).log ≤ ↑d * (Complex.abs z).log
div_le : -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) ≤ t
⊢ 0 < 2 * (Complex.abs z).log
Tactic:
positivity
Proof state after:
no goals
Theorem: f_error_le_generic
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
inner_le : -(1 - 1 / Complex.abs z).log ≤ s / Complex.abs z
dm : 2 * (Complex.abs z).log ≤ ↑d * (Complex.abs z).log
div_le : -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) ≤ t
⊢ 0 ≤ c
Tactic:
positivity
Proof state after:
no goals
Theorem: f_error_le_generic
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
inner_le : -(1 - 1 / Complex.abs z).log ≤ s / Complex.abs z
dm : 2 * (Complex.abs z).log ≤ ↑d * (Complex.abs z).log
div_le : -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) ≤ t
⊢ 0 ≤ (Complex.abs z)⁻¹ * (Complex.abs z).log⁻¹
Tactic:
positivity
Proof state after:
no goals
Theorem: f_error_le_of_z3
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
⊢ f_error d z ≤ 0.699 / (Complex.abs z * (Complex.abs z).log)
Tactic:
refine f_error_le_generic d 3 1.0986 (s := 1.25) (t := 0.1897) (c := 1.1171) _ z3 ?_
Proof state after:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
⊢ exp 1.0986 ≤ 3
Theorem: f_error_le_of_z3
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
⊢ exp 1.0986 ≤ 3
Tactic:
norm_num
Proof state after:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
⊢ (5493 / 5000).exp ≤ 3
Theorem: f_error_le_of_z3
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
⊢ (5493 / 5000).exp ≤ 3
Tactic:
exact (exp_div_lt).le
Proof state after:
no goals
Theorem: f_error_le_of_z4
Proof 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)
Proof state after:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z4 : 4 ≤ Complex.abs z
⊢ exp 1.3862 ≤ 4
Theorem: f_error_le_of_z4
Proof 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
Proof state after:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z4 : 4 ≤ Complex.abs z
⊢ (6931 / 5000).exp ≤ 4
Theorem: f_error_le_of_z4
Proof 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
Proof state after:
no goals
Theorem: f_error_le_of_z4
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z4 : 4 ≤ Complex.abs z
⊢ 3 ≤ 4
Tactic:
norm_num
Proof state after:
no goals
Theorem: f_error_le_of_z4
Proof 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
Proof state after:
no goals
Theorem: f_error_le_of_z4
Proof 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
Proof state after:
no goals
Theorem: f_error_le_of_z4
Proof 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
Proof state after:
no goals
Theorem: f_error_le_of_z4
Proof 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
Proof state after:
no goals
Theorem: f_error_le_of_z4
Proof 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
Proof state after:
no goals
Theorem: f_error_le_of_z4
Proof 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
Proof state after:
no goals
Theorem: f_error_le_of_z6
Proof 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)
Proof state after:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z6 : 6 ≤ Complex.abs z
⊢ exp 1.791 ≤ 6
Theorem: f_error_le_of_z6
Proof 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
Proof state after:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z6 : 6 ≤ Complex.abs z
⊢ (1791 / 1000).exp ≤ 6
Theorem: f_error_le_of_z6
Proof 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
Proof state after:
no goals
Theorem: f_error_le_of_z6
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z6 : 6 ≤ Complex.abs z
⊢ 3 ≤ 6
Tactic:
norm_num
Proof state after:
no goals
Theorem: f_error_le_of_z6
Proof 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
Proof state after:
no goals
Theorem: f_error_le_of_z6
Proof 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
Proof state after:
no goals
Theorem: f_error_le_of_z6
Proof 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
Proof state after:
no goals
Theorem: f_error_le_of_z6
Proof 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
Proof state after:
no goals
Theorem: f_error_le_of_z6
Proof 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
Proof state after:
no goals
Theorem: f_error_le_of_z6
Proof 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
Proof state after:
no goals
Theorem: f_error_le_of_z12
Proof 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)
Proof state after:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z12 : 12 ≤ Complex.abs z
⊢ exp 2.48 ≤ 12
Theorem: f_error_le_of_z12
Proof 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
Proof state after:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z12 : 12 ≤ Complex.abs z
⊢ (62 / 25).exp ≤ 12
Theorem: f_error_le_of_z12
Proof 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
Proof state after:
no goals
Theorem: f_error_le_of_z12
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z12 : 12 ≤ Complex.abs z
⊢ 3 ≤ 12
Tactic:
norm_num
Proof state after:
no goals
Theorem: f_error_le_of_z12
Proof 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
Proof state after:
no goals
Theorem: f_error_le_of_z12
Proof 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
Proof state after:
no goals
Theorem: f_error_le_of_z12
Proof 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
Proof state after:
no goals
Theorem: f_error_le_of_z12
Proof 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
Proof state after:
no goals
Theorem: f_error_le_of_z12
Proof 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
Proof state after:
no goals
Theorem: f_error_le_of_z12
Proof 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
Proof state after:
no goals
Theorem: f_error_le_of_z33
Proof 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)
Proof state after:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z33 : 33 ≤ Complex.abs z
⊢ exp 3.49 ≤ 33
Theorem: f_error_le_of_z33
Proof 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
Proof state after:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z33 : 33 ≤ Complex.abs z
⊢ (349 / 100).exp ≤ 33
Theorem: f_error_le_of_z33
Proof 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
Proof state after:
no goals
Theorem: f_error_le_of_z33
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z33 : 33 ≤ Complex.abs z
⊢ 3 ≤ 33
Tactic:
norm_num
Proof state after:
no goals
Theorem: f_error_le_of_z33
Proof 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
Proof state after:
no goals
Theorem: f_error_le_of_z33
Proof 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
Proof state after:
no goals
Theorem: f_error_le_of_z33
Proof 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
Proof state after:
no goals
Theorem: f_error_le_of_z33
Proof 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
Proof state after:
no goals
Theorem: f_error_le_of_z33
Proof 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
Proof state after:
no goals
Theorem: f_error_le_of_z33
Proof 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
Proof state after:
no goals
Theorem: f_error_le_of_z140
Proof 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)
Proof state after:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z140 : 140 ≤ Complex.abs z
⊢ exp 4.94 ≤ 140
Theorem: f_error_le_of_z140
Proof 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
Proof state after:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z140 : 140 ≤ Complex.abs z
⊢ (247 / 50).exp ≤ 140
Theorem: f_error_le_of_z140
Proof 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
Proof state after:
no goals
Theorem: f_error_le_of_z140
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z140 : 140 ≤ Complex.abs z
⊢ 3 ≤ 140
Tactic:
norm_num
Proof state after:
no goals
Theorem: f_error_le_of_z140
Proof 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
Proof state after:
no goals