internlm/Lean-Github huggingface dataset:
Theorem: potential_error_le'
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ potential_error d c z ≤ 0.8095 / Complex.abs z ^ i
Tactic:
refine le_trans (potential_error_le d b4 bz cz) (div_le_div_of_nonneg_left (by norm_num)
  (by positivity) ?_)
Proof state after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ Complex.abs z ^ i ≤ Complex.abs z ^ (1 + (-0.8095 / (Complex.abs z * (Complex.abs z).log)).exp)
Theorem: potential_error_le'
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ Complex.abs z ^ i ≤ Complex.abs z ^ (1 + (-0.8095 / (Complex.abs z * (Complex.abs z).log)).exp)
Tactic:
refine Real.rpow_le_rpow_of_exponent_le (by linarith) ?_
Proof state after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ i ≤ 1 + (-0.8095 / (Complex.abs z * (Complex.abs z).log)).exp
Theorem: potential_error_le'
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ i ≤ 1 + (-0.8095 / (Complex.abs z * (Complex.abs z).log)).exp
Tactic:
simp only [add_comm (1:ℝ), ←sub_le_iff_le_add]
Proof state after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ i - 1 ≤ (-0.8095 / (Complex.abs z * (Complex.abs z).log)).exp
Theorem: potential_error_le'
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ i - 1 ≤ (-0.8095 / (Complex.abs z * (Complex.abs z).log)).exp
Tactic:
refine le_trans ij (Real.exp_le_exp.mpr ?_)
Proof state after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ -j ≤ -0.8095 / (Complex.abs z * (Complex.abs z).log)
Theorem: potential_error_le'
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ -j ≤ -0.8095 / (Complex.abs z * (Complex.abs z).log)
Tactic:
simp only [neg_div, neg_le_neg_iff, div_mul_eq_div_div]
Proof state after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ 0.8095 / Complex.abs z / (Complex.abs z).log ≤ j
Theorem: potential_error_le'
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ 0.8095 / Complex.abs z / (Complex.abs z).log ≤ j
Tactic:
rw [div_le_iff l0, mul_comm j, ←div_le_iff j0]
Proof state after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ 0.8095 / Complex.abs z / j ≤ (Complex.abs z).log
Theorem: potential_error_le'
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ 0.8095 / Complex.abs z / j ≤ (Complex.abs z).log
Tactic:
trans 0.8095 / b / j
Proof state after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ 0.8095 / Complex.abs z / j ≤ 0.8095 / b / j

c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ 0.8095 / b / j ≤ (Complex.abs z).log
Theorem: potential_error_le'
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
⊢ 0 < Complex.abs z
Tactic:
linarith
Proof state after:
no goals
Theorem: potential_error_le'
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
⊢ 0 < 4
Tactic:
linarith
Proof state after:
no goals
Theorem: potential_error_le'
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
⊢ 4 ≤ Complex.abs z
Tactic:
linarith
Proof state after:
no goals
Theorem: potential_error_le'
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
l1 : 1.386 < (Complex.abs z).log
⊢ 0 < 1.386
Tactic:
norm_num
Proof state after:
no goals
Theorem: potential_error_le'
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ 0 ≤ 0.8095
Tactic:
norm_num
Proof state after:
no goals
Theorem: potential_error_le'
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ 0 < Complex.abs z ^ i
Tactic:
positivity
Proof state after:
no goals
Theorem: potential_error_le'
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ 1 ≤ Complex.abs z
Tactic:
linarith
Proof state after:
no goals
Theorem: potential_error_le'
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ 0.8095 / Complex.abs z / j ≤ 0.8095 / b / j
Tactic:
gcongr
Proof state after:
no goals
Theorem: potential_error_le'
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ 0.8095 / b / j ≤ (Complex.abs z).log
Tactic:
rw [Real.le_log_iff_exp_le z0]
Proof state after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ (0.8095 / b / j).exp ≤ Complex.abs z
Theorem: potential_error_le'
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ (0.8095 / b / j).exp ≤ Complex.abs z
Tactic:
exact le_trans bj bz
Proof state after:
no goals
Theorem: potential_error_le_of_z4
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ potential_error d c z ≤ 0.8095 / Complex.abs z ^ 1.864
Tactic:
apply potential_error_le' d _ (j := 0.146) (b := 4) (by norm_num) z4 cz (by norm_num)
Proof state after:
case ij
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 1.864 - 1 ≤ (-0.146).exp

case bj
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ (0.8095 / 4 / 0.146).exp ≤ 4
Theorem: potential_error_le_of_z4
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 4 ≤ 4
Tactic:
norm_num
Proof state after:
no goals
Theorem: potential_error_le_of_z4
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 0 < 0.146
Tactic:
norm_num
Proof state after:
no goals
Theorem: potential_error_le_of_z4
Proof state before:
case ij
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 1.864 - 1 ≤ (-0.146).exp
Tactic:
norm_num
Proof state after:
case ij
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 108 / 125 ≤ (-(73 / 500)).exp
Theorem: potential_error_le_of_z4
Proof state before:
case ij
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 108 / 125 ≤ (-(73 / 500)).exp
Tactic:
exact (lt_exp_neg_div).le
Proof state after:
no goals
Theorem: potential_error_le_of_z4
Proof state before:
case bj
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ (0.8095 / 4 / 0.146).exp ≤ 4
Tactic:
norm_num
Proof state after:
case bj
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ (1619 / 1168).exp ≤ 4
Theorem: potential_error_le_of_z4
Proof state before:
case bj
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ (1619 / 1168).exp ≤ 4
Tactic:
exact (exp_div_lt).le
Proof state after:
no goals
Theorem: potential_error_le_of_z6
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z6 : 6 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ potential_error d c z ≤ 0.8095 / Complex.abs z ^ 1.927
Tactic:
apply potential_error_le' d _ (j := 0.0753) (b := 6) (by norm_num) z6 cz (by norm_num)
Proof state after:
case ij
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z6 : 6 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 1.927 - 1 ≤ (-753e-4).exp

case bj
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z6 : 6 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ (0.8095 / 6 / 753e-4).exp ≤ 6
Theorem: potential_error_le_of_z6
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z6 : 6 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 4 ≤ 6
Tactic:
norm_num
Proof state after:
no goals
Theorem: potential_error_le_of_z6
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z6 : 6 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 0 < 753e-4
Tactic:
norm_num
Proof state after:
no goals
Theorem: potential_error_le_of_z6
Proof state before:
case ij
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z6 : 6 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 1.927 - 1 ≤ (-753e-4).exp
Tactic:
norm_num
Proof state after:
case ij
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z6 : 6 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 927 / 1000 ≤ (-(753 / 10000)).exp
Theorem: potential_error_le_of_z6
Proof state before:
case ij
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z6 : 6 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 927 / 1000 ≤ (-(753 / 10000)).exp
Tactic:
exact (lt_exp_neg_div).le
Proof state after:
no goals
Theorem: potential_error_le_of_z6
Proof state before:
case bj
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z6 : 6 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ (0.8095 / 6 / 753e-4).exp ≤ 6
Tactic:
norm_num
Proof state after:
case bj
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z6 : 6 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ (8095 / 4518).exp ≤ 6
Theorem: potential_error_le_of_z6
Proof state before:
case bj
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z6 : 6 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ (8095 / 4518).exp ≤ 6
Tactic:
exact (exp_div_lt).le
Proof state after:
no goals
Theorem: iter_error_le_log_log_abs
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ iter_error d c z ≤ (Complex.abs z).log.log
Tactic:
have hl : 1.38 ≤ log (abs z) := by
  rw [Real.le_log_iff_exp_le (by positivity)]
  norm_num
  exact le_trans (exp_div_lt).le z4
Proof state after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
hl : 1.38 ≤ (Complex.abs z).log
⊢ iter_error d c z ≤ (Complex.abs z).log.log
Theorem: iter_error_le_log_log_abs
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
hl : 1.38 ≤ (Complex.abs z).log
⊢ iter_error d c z ≤ (Complex.abs z).log.log
Tactic:
have hll : 0.32 ≤ log (log (abs z)) := by
  rw [Real.le_log_iff_exp_le (by positivity)]
  norm_num
  exact le_trans (exp_div_lt).le hl
Proof state after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
hl : 1.38 ≤ (Complex.abs z).log
hll : 0.32 ≤ (Complex.abs z).log.log
⊢ iter_error d c z ≤ (Complex.abs z).log.log
Theorem: iter_error_le_log_log_abs
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
hl : 1.38 ≤ (Complex.abs z).log
hll : 0.32 ≤ (Complex.abs z).log.log
⊢ iter_error d c z ≤ (Complex.abs z).log.log
Tactic:
refine le_trans ?_ hll
Proof state after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
hl : 1.38 ≤ (Complex.abs z).log
hll : 0.32 ≤ (Complex.abs z).log.log
⊢ iter_error d c z ≤ 0.32
Theorem: iter_error_le_log_log_abs
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
hl : 1.38 ≤ (Complex.abs z).log
hll : 0.32 ≤ (Complex.abs z).log.log
⊢ iter_error d c z ≤ 0.32
Tactic:
apply le_trans (iter_error_le_of_z4 d z4 cz)
Proof state after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
hl : 1.38 ≤ (Complex.abs z).log
hll : 0.32 ≤ (Complex.abs z).log.log
⊢ 0.8095 / (Complex.abs z * (Complex.abs z).log) ≤ 0.32
Theorem: iter_error_le_log_log_abs
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
hl : 1.38 ≤ (Complex.abs z).log
hll : 0.32 ≤ (Complex.abs z).log.log
⊢ 0.8095 / (Complex.abs z * (Complex.abs z).log) ≤ 0.32
Tactic:
rw [div_le_iff' (by positivity), ←div_le_iff (by norm_num)]
Proof state after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
hl : 1.38 ≤ (Complex.abs z).log
hll : 0.32 ≤ (Complex.abs z).log.log
⊢ 0.8095 / 0.32 ≤ Complex.abs z * (Complex.abs z).log
Theorem: iter_error_le_log_log_abs
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
hl : 1.38 ≤ (Complex.abs z).log
hll : 0.32 ≤ (Complex.abs z).log.log
⊢ 0.8095 / 0.32 ≤ Complex.abs z * (Complex.abs z).log
Tactic:
refine le_trans (by norm_num) (mul_le_mul z4 hl (by positivity) (by positivity))
Proof state after:
no goals
Theorem: iter_error_le_log_log_abs
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 1.38 ≤ (Complex.abs z).log
Tactic:
rw [Real.le_log_iff_exp_le (by positivity)]
Proof state after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ exp 1.38 ≤ Complex.abs z
Theorem: iter_error_le_log_log_abs
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ exp 1.38 ≤ Complex.abs z
Tactic:
norm_num
Proof state after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ (69 / 50).exp ≤ Complex.abs z
Theorem: iter_error_le_log_log_abs
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ (69 / 50).exp ≤ Complex.abs z
Tactic:
exact le_trans (exp_div_lt).le z4
Proof state after:
no goals
Theorem: iter_error_le_log_log_abs
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 0 < Complex.abs z
Tactic:
positivity
Proof state after:
no goals
Theorem: iter_error_le_log_log_abs
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
hl : 1.38 ≤ (Complex.abs z).log
⊢ 0.32 ≤ (Complex.abs z).log.log
Tactic:
rw [Real.le_log_iff_exp_le (by positivity)]
Proof state after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
hl : 1.38 ≤ (Complex.abs z).log
⊢ exp 0.32 ≤ (Complex.abs z).log
Theorem: iter_error_le_log_log_abs
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
hl : 1.38 ≤ (Complex.abs z).log
⊢ exp 0.32 ≤ (Complex.abs z).log
Tactic:
norm_num
Proof state after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
hl : 1.38 ≤ (Complex.abs z).log
⊢ (8 / 25).exp ≤ (Complex.abs z).log
Theorem: iter_error_le_log_log_abs
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
hl : 1.38 ≤ (Complex.abs z).log
⊢ (8 / 25).exp ≤ (Complex.abs z).log
Tactic:
exact le_trans (exp_div_lt).le hl
Proof state after:
no goals
Theorem: iter_error_le_log_log_abs
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
hl : 1.38 ≤ (Complex.abs z).log
⊢ 0 < (Complex.abs z).log
Tactic:
positivity
Proof state after:
no goals
Theorem: iter_error_le_log_log_abs
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
hl : 1.38 ≤ (Complex.abs z).log
hll : 0.32 ≤ (Complex.abs z).log.log
⊢ 0 < Complex.abs z * (Complex.abs z).log
Tactic:
positivity
Proof state after:
no goals
Theorem: iter_error_le_log_log_abs
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
hl : 1.38 ≤ (Complex.abs z).log
hll : 0.32 ≤ (Complex.abs z).log.log
⊢ 0 < 0.32
Tactic:
norm_num
Proof state after:
no goals
Theorem: iter_error_le_log_log_abs
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
hl : 1.38 ≤ (Complex.abs z).log
hll : 0.32 ≤ (Complex.abs z).log.log
⊢ 0.8095 / 0.32 ≤ 4 * 1.38
Tactic:
norm_num
Proof state after:
no goals
Theorem: iter_error_le_log_log_abs
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
hl : 1.38 ≤ (Complex.abs z).log
hll : 0.32 ≤ (Complex.abs z).log.log
⊢ 0 ≤ 1.38
Tactic:
positivity
Proof state after:
no goals
Theorem: iter_error_le_log_log_abs
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
hl : 1.38 ≤ (Complex.abs z).log
hll : 0.32 ≤ (Complex.abs z).log.log
⊢ 0 ≤ Complex.abs z
Tactic:
positivity
Proof state after:
no goals