internlm/Lean-Github huggingface dataset:
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
lb : l.exp ≤ b
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✝
⊢ f_error d z ≤ g / (Complex.abs z * (Complex.abs z).log)
Tactic:
have z3 := le_trans b3 bz
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
lb : l.exp ≤ b
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
⊢ f_error d z ≤ g / (Complex.abs z * (Complex.abs z).log)
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
lb : l.exp ≤ b
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
⊢ f_error d z ≤ g / (Complex.abs z * (Complex.abs z).log)
Tactic:
replace lb := (Real.le_log_iff_exp_le (by positivity)).mpr (le_trans lb bz)
Proof state after:
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
⊢ f_error d z ≤ g / (Complex.abs z * (Complex.abs z).log)
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
⊢ f_error d z ≤ g / (Complex.abs z * (Complex.abs z).log)
Tactic:
have l0' : 0 < log (abs z) := trans l0 lb
Proof state after:
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
⊢ f_error d z ≤ g / (Complex.abs z * (Complex.abs z).log)
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
⊢ f_error d z ≤ g / (Complex.abs z * (Complex.abs z).log)
Tactic:
have inner_le : -log (1 - 1 / abs z) ≤ s / abs z := by
  rw [one_div, div_eq_mul_inv]
  apply neg_log_one_sub_le_linear (by positivity) s1
  exact le_trans (inv_le_inv_of_le (by positivity) bz) bs
Proof state after:
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
⊢ f_error d z ≤ g / (Complex.abs z * (Complex.abs z).log)
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
⊢ f_error d z ≤ g / (Complex.abs z * (Complex.abs z).log)
Tactic:
have dm : 2 * log (abs z) ≤ d * log (abs z) := by bound
Proof state after:
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
⊢ f_error d z ≤ g / (Complex.abs z * (Complex.abs z).log)
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
⊢ f_error d z ≤ g / (Complex.abs z * (Complex.abs z).log)
Tactic:
have div_le : -log (1 - 1 / abs z) / (d * log (abs z)) ≤ t := by
  have sz : s / abs z ≤ s / b := div_le_div_of_nonneg_left (by positivity) (by positivity) bz
  exact le_trans (div_le_div (by positivity) (le_trans inner_le sz) (by positivity)
    (le_trans (mul_le_mul_of_nonneg_left lb (by norm_num)) dm)) st
Proof state after:
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
⊢ f_error d z ≤ g / (Complex.abs z * (Complex.abs z).log)
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
⊢ f_error d z ≤ g / (Complex.abs z * (Complex.abs z).log)
Tactic:
refine le_trans (neg_log_one_sub_le_linear (f_error_inner_nonneg d z3) c1 ?_) ?_
Proof state after:
case refine_1
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 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹

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)
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
lb : l.exp ≤ b
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
⊢ 0 < 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
⊢ -(1 - 1 / Complex.abs z).log ≤ s / Complex.abs z
Tactic:
rw [one_div, div_eq_mul_inv]
Proof state after:
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
⊢ -(1 - (Complex.abs z)⁻¹).log ≤ s * (Complex.abs z)⁻¹
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
⊢ -(1 - (Complex.abs z)⁻¹).log ≤ s * (Complex.abs z)⁻¹
Tactic:
apply neg_log_one_sub_le_linear (by positivity) s1
Proof state after:
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
⊢ (Complex.abs z)⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹
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
⊢ (Complex.abs z)⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹
Tactic:
exact le_trans (inv_le_inv_of_le (by positivity) bz) bs
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
⊢ 0 ≤ (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
⊢ 0 < b
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
⊢ 2 * (Complex.abs z).log ≤ ↑d * (Complex.abs z).log
Tactic:
bound
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
⊢ -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) ≤ t
Tactic:
have sz : s / abs z ≤ s / b := div_le_div_of_nonneg_left (by positivity) (by positivity) bz
Proof state after:
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
sz : s / Complex.abs z ≤ s / b
⊢ -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) ≤ t
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
sz : s / Complex.abs z ≤ s / b
⊢ -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) ≤ t
Tactic:
exact le_trans (div_le_div (by positivity) (le_trans inner_le sz) (by positivity)
  (le_trans (mul_le_mul_of_nonneg_left lb (by norm_num)) dm)) st
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
⊢ 0 ≤ s
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
⊢ 0 < b
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
sz : s / Complex.abs z ≤ s / b
⊢ 0 ≤ s / b
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
sz : s / Complex.abs z ≤ s / b
⊢ 0 < 2 * l
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
sz : s / Complex.abs z ≤ s / b
⊢ 0 ≤ 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: f_error_le_generic
Proof state before:
case refine_1
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 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
Tactic:
exact le_trans div_le tc
Proof state after:
no goals