internlm/Lean-Github huggingface dataset:
Theorem: iter_error_le
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
i b s0 s1 s2 : ℝ
c : ℂ
b3 : 3 ≤ b
s1p : 0 ≤ s1
s2p : 0 ≤ s2
bs0 : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s0 / (Complex.abs w * (Complex.abs w).log)
bs1 : ∀ {w : ℂ}, (b ^ (d - 1) - 1) * b ≤ Complex.abs w → f_error d w ≤ s1 / (Complex.abs w * (Complex.abs w).log)
b0' : 0 < b ^ (d - 1) - 1
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
b0 : 0 < b
z0 : 0 < Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 1 < (Complex.abs z).log
bb : ℝ
hbb : (b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1 = bb
b11 : 11 ≤ bb
bb3 : 3 ≤ bb * b
bs2 : ∀ {w : ℂ}, bb * b ≤ Complex.abs w → f_error d w ≤ s2 / (Complex.abs w * (Complex.abs w).log)
b0'' : 0 < 1 - (bb * b - 1)⁻¹
si : s0 + s1 / (b ^ (d - 1) - 1) + s2 / ((1 - (bb * b - 1)⁻¹) * bb) ≤ i
fz : Complex.abs z ^ d - Complex.abs c ≤ Complex.abs (f' d c z)
⊢ (Complex.abs z ^ (d - 1) - 1) * Complex.abs z ≥ (b ^ (d - 1) - 1) * Complex.abs z
Tactic:
bound
Proof state after:
no goals
Theorem: iter_error_le
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
i b s0 s1 s2 : ℝ
c : ℂ
b3 : 3 ≤ b
s1p : 0 ≤ s1
s2p : 0 ≤ s2
bs0 : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s0 / (Complex.abs w * (Complex.abs w).log)
bs1 : ∀ {w : ℂ}, (b ^ (d - 1) - 1) * b ≤ Complex.abs w → f_error d w ≤ s1 / (Complex.abs w * (Complex.abs w).log)
b0' : 0 < b ^ (d - 1) - 1
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
b0 : 0 < b
z0 : 0 < Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 1 < (Complex.abs z).log
bb : ℝ
hbb : (b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1 = bb
b11 : 11 ≤ bb
bb3 : 3 ≤ bb * b
bs2 : ∀ {w : ℂ}, bb * b ≤ Complex.abs w → f_error d w ≤ s2 / (Complex.abs w * (Complex.abs w).log)
b0'' : 0 < 1 - (bb * b - 1)⁻¹
si : s0 + s1 / (b ^ (d - 1) - 1) + s2 / ((1 - (bb * b - 1)⁻¹) * bb) ≤ i
fz : Complex.abs z ^ d - Complex.abs c ≤ Complex.abs (f' d c z)
fz' : (b ^ (d - 1) - 1) * Complex.abs z ≤ Complex.abs (f' d c z)
zfz : Complex.abs z ≤ Complex.abs (f' d c z)
zffz : Complex.abs z ≤ Complex.abs (f' d c (f' d c z))
bfz : b ≤ Complex.abs (f' d c z)
⊢ bb * Complex.abs z ≤ Complex.abs (f' d c (f' d c z))
Tactic:
calc abs ((f' d c z)^d + c)
  _ ≥ abs ((f' d c z)^d) - abs c := by bound
  _ = (abs (f' d c z))^d - abs c := by rw [Complex.abs.map_pow]
  _ ≥ ((b^(d-1)-1) * abs z)^d - abs z := by bound
  _ = (b^(d-1)-1)^d * (abs z)^(d-1) * abs z - abs z := by
      rw [mul_assoc, ←pow_succ, mul_pow, Nat.sub_add_cancel (d_ge_one d)]
  _ ≥ (b^(d-1)-1)^d * b^(d-1) * abs z - abs z := by bound
  _ = bb * abs z := by rw [←hbb, sub_one_mul]
Proof state after:
no goals
Theorem: iter_error_le
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
i b s0 s1 s2 : ℝ
c : ℂ
b3 : 3 ≤ b
s1p : 0 ≤ s1
s2p : 0 ≤ s2
bs0 : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s0 / (Complex.abs w * (Complex.abs w).log)
bs1 : ∀ {w : ℂ}, (b ^ (d - 1) - 1) * b ≤ Complex.abs w → f_error d w ≤ s1 / (Complex.abs w * (Complex.abs w).log)
b0' : 0 < b ^ (d - 1) - 1
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
b0 : 0 < b
z0 : 0 < Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 1 < (Complex.abs z).log
bb : ℝ
hbb : (b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1 = bb
b11 : 11 ≤ bb
bb3 : 3 ≤ bb * b
bs2 : ∀ {w : ℂ}, bb * b ≤ Complex.abs w → f_error d w ≤ s2 / (Complex.abs w * (Complex.abs w).log)
b0'' : 0 < 1 - (bb * b - 1)⁻¹
si : s0 + s1 / (b ^ (d - 1) - 1) + s2 / ((1 - (bb * b - 1)⁻¹) * bb) ≤ i
fz : Complex.abs z ^ d - Complex.abs c ≤ Complex.abs (f' d c z)
fz' : (b ^ (d - 1) - 1) * Complex.abs z ≤ Complex.abs (f' d c z)
zfz : Complex.abs z ≤ Complex.abs (f' d c z)
zffz : Complex.abs z ≤ Complex.abs (f' d c (f' d c z))
bfz : b ≤ Complex.abs (f' d c z)
⊢ Complex.abs (f' d c z ^ d + c) ≥ Complex.abs (f' d c z ^ d) - Complex.abs c
Tactic:
bound
Proof state after:
no goals
Theorem: iter_error_le
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
i b s0 s1 s2 : ℝ
c : ℂ
b3 : 3 ≤ b
s1p : 0 ≤ s1
s2p : 0 ≤ s2
bs0 : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s0 / (Complex.abs w * (Complex.abs w).log)
bs1 : ∀ {w : ℂ}, (b ^ (d - 1) - 1) * b ≤ Complex.abs w → f_error d w ≤ s1 / (Complex.abs w * (Complex.abs w).log)
b0' : 0 < b ^ (d - 1) - 1
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
b0 : 0 < b
z0 : 0 < Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 1 < (Complex.abs z).log
bb : ℝ
hbb : (b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1 = bb
b11 : 11 ≤ bb
bb3 : 3 ≤ bb * b
bs2 : ∀ {w : ℂ}, bb * b ≤ Complex.abs w → f_error d w ≤ s2 / (Complex.abs w * (Complex.abs w).log)
b0'' : 0 < 1 - (bb * b - 1)⁻¹
si : s0 + s1 / (b ^ (d - 1) - 1) + s2 / ((1 - (bb * b - 1)⁻¹) * bb) ≤ i
fz : Complex.abs z ^ d - Complex.abs c ≤ Complex.abs (f' d c z)
fz' : (b ^ (d - 1) - 1) * Complex.abs z ≤ Complex.abs (f' d c z)
zfz : Complex.abs z ≤ Complex.abs (f' d c z)
zffz : Complex.abs z ≤ Complex.abs (f' d c (f' d c z))
bfz : b ≤ Complex.abs (f' d c z)
⊢ Complex.abs (f' d c z ^ d) - Complex.abs c = Complex.abs (f' d c z) ^ d - Complex.abs c
Tactic:
rw [Complex.abs.map_pow]
Proof state after:
no goals
Theorem: iter_error_le
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
i b s0 s1 s2 : ℝ
c : ℂ
b3 : 3 ≤ b
s1p : 0 ≤ s1
s2p : 0 ≤ s2
bs0 : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s0 / (Complex.abs w * (Complex.abs w).log)
bs1 : ∀ {w : ℂ}, (b ^ (d - 1) - 1) * b ≤ Complex.abs w → f_error d w ≤ s1 / (Complex.abs w * (Complex.abs w).log)
b0' : 0 < b ^ (d - 1) - 1
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
b0 : 0 < b
z0 : 0 < Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 1 < (Complex.abs z).log
bb : ℝ
hbb : (b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1 = bb
b11 : 11 ≤ bb
bb3 : 3 ≤ bb * b
bs2 : ∀ {w : ℂ}, bb * b ≤ Complex.abs w → f_error d w ≤ s2 / (Complex.abs w * (Complex.abs w).log)
b0'' : 0 < 1 - (bb * b - 1)⁻¹
si : s0 + s1 / (b ^ (d - 1) - 1) + s2 / ((1 - (bb * b - 1)⁻¹) * bb) ≤ i
fz : Complex.abs z ^ d - Complex.abs c ≤ Complex.abs (f' d c z)
fz' : (b ^ (d - 1) - 1) * Complex.abs z ≤ Complex.abs (f' d c z)
zfz : Complex.abs z ≤ Complex.abs (f' d c z)
zffz : Complex.abs z ≤ Complex.abs (f' d c (f' d c z))
bfz : b ≤ Complex.abs (f' d c z)
⊢ Complex.abs (f' d c z) ^ d - Complex.abs c ≥ ((b ^ (d - 1) - 1) * Complex.abs z) ^ d - Complex.abs z
Tactic:
bound
Proof state after:
no goals
Theorem: iter_error_le
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
i b s0 s1 s2 : ℝ
c : ℂ
b3 : 3 ≤ b
s1p : 0 ≤ s1
s2p : 0 ≤ s2
bs0 : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s0 / (Complex.abs w * (Complex.abs w).log)
bs1 : ∀ {w : ℂ}, (b ^ (d - 1) - 1) * b ≤ Complex.abs w → f_error d w ≤ s1 / (Complex.abs w * (Complex.abs w).log)
b0' : 0 < b ^ (d - 1) - 1
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
b0 : 0 < b
z0 : 0 < Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 1 < (Complex.abs z).log
bb : ℝ
hbb : (b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1 = bb
b11 : 11 ≤ bb
bb3 : 3 ≤ bb * b
bs2 : ∀ {w : ℂ}, bb * b ≤ Complex.abs w → f_error d w ≤ s2 / (Complex.abs w * (Complex.abs w).log)
b0'' : 0 < 1 - (bb * b - 1)⁻¹
si : s0 + s1 / (b ^ (d - 1) - 1) + s2 / ((1 - (bb * b - 1)⁻¹) * bb) ≤ i
fz : Complex.abs z ^ d - Complex.abs c ≤ Complex.abs (f' d c z)
fz' : (b ^ (d - 1) - 1) * Complex.abs z ≤ Complex.abs (f' d c z)
zfz : Complex.abs z ≤ Complex.abs (f' d c z)
zffz : Complex.abs z ≤ Complex.abs (f' d c (f' d c z))
bfz : b ≤ Complex.abs (f' d c z)
⊢ ((b ^ (d - 1) - 1) * Complex.abs z) ^ d - Complex.abs z =
    (b ^ (d - 1) - 1) ^ d * Complex.abs z ^ (d - 1) * Complex.abs z - Complex.abs z
Tactic:
rw [mul_assoc, ←pow_succ, mul_pow, Nat.sub_add_cancel (d_ge_one d)]
Proof state after:
no goals
Theorem: iter_error_le
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
i b s0 s1 s2 : ℝ
c : ℂ
b3 : 3 ≤ b
s1p : 0 ≤ s1
s2p : 0 ≤ s2
bs0 : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s0 / (Complex.abs w * (Complex.abs w).log)
bs1 : ∀ {w : ℂ}, (b ^ (d - 1) - 1) * b ≤ Complex.abs w → f_error d w ≤ s1 / (Complex.abs w * (Complex.abs w).log)
b0' : 0 < b ^ (d - 1) - 1
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
b0 : 0 < b
z0 : 0 < Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 1 < (Complex.abs z).log
bb : ℝ
hbb : (b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1 = bb
b11 : 11 ≤ bb
bb3 : 3 ≤ bb * b
bs2 : ∀ {w : ℂ}, bb * b ≤ Complex.abs w → f_error d w ≤ s2 / (Complex.abs w * (Complex.abs w).log)
b0'' : 0 < 1 - (bb * b - 1)⁻¹
si : s0 + s1 / (b ^ (d - 1) - 1) + s2 / ((1 - (bb * b - 1)⁻¹) * bb) ≤ i
fz : Complex.abs z ^ d - Complex.abs c ≤ Complex.abs (f' d c z)
fz' : (b ^ (d - 1) - 1) * Complex.abs z ≤ Complex.abs (f' d c z)
zfz : Complex.abs z ≤ Complex.abs (f' d c z)
zffz : Complex.abs z ≤ Complex.abs (f' d c (f' d c z))
bfz : b ≤ Complex.abs (f' d c z)
⊢ (b ^ (d - 1) - 1) ^ d * Complex.abs z ^ (d - 1) * Complex.abs z - Complex.abs z ≥
    (b ^ (d - 1) - 1) ^ d * b ^ (d - 1) * Complex.abs z - Complex.abs z
Tactic:
bound
Proof state after:
no goals
Theorem: iter_error_le
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
i b s0 s1 s2 : ℝ
c : ℂ
b3 : 3 ≤ b
s1p : 0 ≤ s1
s2p : 0 ≤ s2
bs0 : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s0 / (Complex.abs w * (Complex.abs w).log)
bs1 : ∀ {w : ℂ}, (b ^ (d - 1) - 1) * b ≤ Complex.abs w → f_error d w ≤ s1 / (Complex.abs w * (Complex.abs w).log)
b0' : 0 < b ^ (d - 1) - 1
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
b0 : 0 < b
z0 : 0 < Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 1 < (Complex.abs z).log
bb : ℝ
hbb : (b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1 = bb
b11 : 11 ≤ bb
bb3 : 3 ≤ bb * b
bs2 : ∀ {w : ℂ}, bb * b ≤ Complex.abs w → f_error d w ≤ s2 / (Complex.abs w * (Complex.abs w).log)
b0'' : 0 < 1 - (bb * b - 1)⁻¹
si : s0 + s1 / (b ^ (d - 1) - 1) + s2 / ((1 - (bb * b - 1)⁻¹) * bb) ≤ i
fz : Complex.abs z ^ d - Complex.abs c ≤ Complex.abs (f' d c z)
fz' : (b ^ (d - 1) - 1) * Complex.abs z ≤ Complex.abs (f' d c z)
zfz : Complex.abs z ≤ Complex.abs (f' d c z)
zffz : Complex.abs z ≤ Complex.abs (f' d c (f' d c z))
bfz : b ≤ Complex.abs (f' d c z)
⊢ (b ^ (d - 1) - 1) ^ d * b ^ (d - 1) * Complex.abs z - Complex.abs z = bb * Complex.abs z
Tactic:
rw [←hbb, sub_one_mul]
Proof state after:
no goals
Theorem: iter_error_le
Proof state before:
case refine_1
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
i b s0 s1 s2 : ℝ
c : ℂ
b3 : 3 ≤ b
s1p : 0 ≤ s1
s2p : 0 ≤ s2
bs0 : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s0 / (Complex.abs w * (Complex.abs w).log)
bs1 : ∀ {w : ℂ}, (b ^ (d - 1) - 1) * b ≤ Complex.abs w → f_error d w ≤ s1 / (Complex.abs w * (Complex.abs w).log)
b0' : 0 < b ^ (d - 1) - 1
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
b0 : 0 < b
z0 : 0 < Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 1 < (Complex.abs z).log
bb : ℝ
hbb : (b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1 = bb
b11 : 11 ≤ bb
bb3 : 3 ≤ bb * b
bs2 : ∀ {w : ℂ}, bb * b ≤ Complex.abs w → f_error d w ≤ s2 / (Complex.abs w * (Complex.abs w).log)
b0'' : 0 < 1 - (bb * b - 1)⁻¹
si : s0 + s1 / (b ^ (d - 1) - 1) + s2 / ((1 - (bb * b - 1)⁻¹) * bb) ≤ i
fz : Complex.abs z ^ d - Complex.abs c ≤ Complex.abs (f' d c z)
fz' : (b ^ (d - 1) - 1) * Complex.abs z ≤ Complex.abs (f' d c z)
zfz : Complex.abs z ≤ Complex.abs (f' d c z)
zffz : Complex.abs z ≤ Complex.abs (f' d c (f' d c z))
bfz : b ≤ Complex.abs (f' d c z)
ffz : bb * Complex.abs z ≤ Complex.abs (f' d c (f' d c z))
e0 : f_error d z ≤ s0 / (Complex.abs z * (Complex.abs z).log)
⊢ (b ^ (d - 1) - 1) * b ≤ Complex.abs (f' d c z)
Tactic:
exact le_trans (mul_le_mul_of_nonneg_left bz b0'.le) fz'
Proof state after:
no goals
Theorem: iter_error_le
Proof state before:
case refine_2
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
i b s0 s1 s2 : ℝ
c : ℂ
b3 : 3 ≤ b
s1p : 0 ≤ s1
s2p : 0 ≤ s2
bs0 : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s0 / (Complex.abs w * (Complex.abs w).log)
bs1 : ∀ {w : ℂ}, (b ^ (d - 1) - 1) * b ≤ Complex.abs w → f_error d w ≤ s1 / (Complex.abs w * (Complex.abs w).log)
b0' : 0 < b ^ (d - 1) - 1
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
b0 : 0 < b
z0 : 0 < Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 1 < (Complex.abs z).log
bb : ℝ
hbb : (b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1 = bb
b11 : 11 ≤ bb
bb3 : 3 ≤ bb * b
bs2 : ∀ {w : ℂ}, bb * b ≤ Complex.abs w → f_error d w ≤ s2 / (Complex.abs w * (Complex.abs w).log)
b0'' : 0 < 1 - (bb * b - 1)⁻¹
si : s0 + s1 / (b ^ (d - 1) - 1) + s2 / ((1 - (bb * b - 1)⁻¹) * bb) ≤ i
fz : Complex.abs z ^ d - Complex.abs c ≤ Complex.abs (f' d c z)
fz' : (b ^ (d - 1) - 1) * Complex.abs z ≤ Complex.abs (f' d c z)
zfz : Complex.abs z ≤ Complex.abs (f' d c z)
zffz : Complex.abs z ≤ Complex.abs (f' d c (f' d c z))
bfz : b ≤ Complex.abs (f' d c z)
ffz : bb * Complex.abs z ≤ Complex.abs (f' d c (f' d c z))
e0 : f_error d z ≤ s0 / (Complex.abs z * (Complex.abs z).log)
⊢ s1 / (Complex.abs (f' d c z) * (Complex.abs (f' d c z)).log) ≤
    s1 / (b ^ (d - 1) - 1) / (Complex.abs z * (Complex.abs z).log)
Tactic:
simp only [div_eq_mul_inv, mul_inv, ←mul_assoc _ (abs z)⁻¹, mul_assoc s1 _ (abs z)⁻¹]
Proof state after:
case refine_2
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
i b s0 s1 s2 : ℝ
c : ℂ
b3 : 3 ≤ b
s1p : 0 ≤ s1
s2p : 0 ≤ s2
bs0 : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s0 / (Complex.abs w * (Complex.abs w).log)
bs1 : ∀ {w : ℂ}, (b ^ (d - 1) - 1) * b ≤ Complex.abs w → f_error d w ≤ s1 / (Complex.abs w * (Complex.abs w).log)
b0' : 0 < b ^ (d - 1) - 1
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
b0 : 0 < b
z0 : 0 < Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 1 < (Complex.abs z).log
bb : ℝ
hbb : (b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1 = bb
b11 : 11 ≤ bb
bb3 : 3 ≤ bb * b
bs2 : ∀ {w : ℂ}, bb * b ≤ Complex.abs w → f_error d w ≤ s2 / (Complex.abs w * (Complex.abs w).log)
b0'' : 0 < 1 - (bb * b - 1)⁻¹
si : s0 + s1 / (b ^ (d - 1) - 1) + s2 / ((1 - (bb * b - 1)⁻¹) * bb) ≤ i
fz : Complex.abs z ^ d - Complex.abs c ≤ Complex.abs (f' d c z)
fz' : (b ^ (d - 1) - 1) * Complex.abs z ≤ Complex.abs (f' d c z)
zfz : Complex.abs z ≤ Complex.abs (f' d c z)
zffz : Complex.abs z ≤ Complex.abs (f' d c (f' d c z))
bfz : b ≤ Complex.abs (f' d c z)
ffz : bb * Complex.abs z ≤ Complex.abs (f' d c (f' d c z))
e0 : f_error d z ≤ s0 / (Complex.abs z * (Complex.abs z).log)
⊢ s1 * ((Complex.abs (f' d c z))⁻¹ * (Complex.abs (f' d c z)).log⁻¹) ≤
    s1 * ((b ^ (d - 1) - 1)⁻¹ * (Complex.abs z)⁻¹) * (Complex.abs z).log⁻¹
Theorem: iter_error_le
Proof state before:
case refine_2
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
i b s0 s1 s2 : ℝ
c : ℂ
b3 : 3 ≤ b
s1p : 0 ≤ s1
s2p : 0 ≤ s2
bs0 : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s0 / (Complex.abs w * (Complex.abs w).log)
bs1 : ∀ {w : ℂ}, (b ^ (d - 1) - 1) * b ≤ Complex.abs w → f_error d w ≤ s1 / (Complex.abs w * (Complex.abs w).log)
b0' : 0 < b ^ (d - 1) - 1
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
b0 : 0 < b
z0 : 0 < Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 1 < (Complex.abs z).log
bb : ℝ
hbb : (b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1 = bb
b11 : 11 ≤ bb
bb3 : 3 ≤ bb * b
bs2 : ∀ {w : ℂ}, bb * b ≤ Complex.abs w → f_error d w ≤ s2 / (Complex.abs w * (Complex.abs w).log)
b0'' : 0 < 1 - (bb * b - 1)⁻¹
si : s0 + s1 / (b ^ (d - 1) - 1) + s2 / ((1 - (bb * b - 1)⁻¹) * bb) ≤ i
fz : Complex.abs z ^ d - Complex.abs c ≤ Complex.abs (f' d c z)
fz' : (b ^ (d - 1) - 1) * Complex.abs z ≤ Complex.abs (f' d c z)
zfz : Complex.abs z ≤ Complex.abs (f' d c z)
zffz : Complex.abs z ≤ Complex.abs (f' d c (f' d c z))
bfz : b ≤ Complex.abs (f' d c z)
ffz : bb * Complex.abs z ≤ Complex.abs (f' d c (f' d c z))
e0 : f_error d z ≤ s0 / (Complex.abs z * (Complex.abs z).log)
⊢ s1 * ((Complex.abs (f' d c z))⁻¹ * (Complex.abs (f' d c z)).log⁻¹) ≤
    s1 * ((b ^ (d - 1) - 1)⁻¹ * (Complex.abs z)⁻¹) * (Complex.abs z).log⁻¹
Tactic:
simp only [←mul_inv, mul_assoc s1]
Proof state after:
case refine_2
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
i b s0 s1 s2 : ℝ
c : ℂ
b3 : 3 ≤ b
s1p : 0 ≤ s1
s2p : 0 ≤ s2
bs0 : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s0 / (Complex.abs w * (Complex.abs w).log)
bs1 : ∀ {w : ℂ}, (b ^ (d - 1) - 1) * b ≤ Complex.abs w → f_error d w ≤ s1 / (Complex.abs w * (Complex.abs w).log)
b0' : 0 < b ^ (d - 1) - 1
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
b0 : 0 < b
z0 : 0 < Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 1 < (Complex.abs z).log
bb : ℝ
hbb : (b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1 = bb
b11 : 11 ≤ bb
bb3 : 3 ≤ bb * b
bs2 : ∀ {w : ℂ}, bb * b ≤ Complex.abs w → f_error d w ≤ s2 / (Complex.abs w * (Complex.abs w).log)
b0'' : 0 < 1 - (bb * b - 1)⁻¹
si : s0 + s1 / (b ^ (d - 1) - 1) + s2 / ((1 - (bb * b - 1)⁻¹) * bb) ≤ i
fz : Complex.abs z ^ d - Complex.abs c ≤ Complex.abs (f' d c z)
fz' : (b ^ (d - 1) - 1) * Complex.abs z ≤ Complex.abs (f' d c z)
zfz : Complex.abs z ≤ Complex.abs (f' d c z)
zffz : Complex.abs z ≤ Complex.abs (f' d c (f' d c z))
bfz : b ≤ Complex.abs (f' d c z)
ffz : bb * Complex.abs z ≤ Complex.abs (f' d c (f' d c z))
e0 : f_error d z ≤ s0 / (Complex.abs z * (Complex.abs z).log)
⊢ s1 * (Complex.abs (f' d c z) * (Complex.abs (f' d c z)).log)⁻¹ ≤
    s1 * ((b ^ (d - 1) - 1) * Complex.abs z * (Complex.abs z).log)⁻¹
Theorem: iter_error_le
Proof state before:
case refine_2
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
i b s0 s1 s2 : ℝ
c : ℂ
b3 : 3 ≤ b
s1p : 0 ≤ s1
s2p : 0 ≤ s2
bs0 : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s0 / (Complex.abs w * (Complex.abs w).log)
bs1 : ∀ {w : ℂ}, (b ^ (d - 1) - 1) * b ≤ Complex.abs w → f_error d w ≤ s1 / (Complex.abs w * (Complex.abs w).log)
b0' : 0 < b ^ (d - 1) - 1
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
b0 : 0 < b
z0 : 0 < Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 1 < (Complex.abs z).log
bb : ℝ
hbb : (b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1 = bb
b11 : 11 ≤ bb
bb3 : 3 ≤ bb * b
bs2 : ∀ {w : ℂ}, bb * b ≤ Complex.abs w → f_error d w ≤ s2 / (Complex.abs w * (Complex.abs w).log)
b0'' : 0 < 1 - (bb * b - 1)⁻¹
si : s0 + s1 / (b ^ (d - 1) - 1) + s2 / ((1 - (bb * b - 1)⁻¹) * bb) ≤ i
fz : Complex.abs z ^ d - Complex.abs c ≤ Complex.abs (f' d c z)
fz' : (b ^ (d - 1) - 1) * Complex.abs z ≤ Complex.abs (f' d c z)
zfz : Complex.abs z ≤ Complex.abs (f' d c z)
zffz : Complex.abs z ≤ Complex.abs (f' d c (f' d c z))
bfz : b ≤ Complex.abs (f' d c z)
ffz : bb * Complex.abs z ≤ Complex.abs (f' d c (f' d c z))
e0 : f_error d z ≤ s0 / (Complex.abs z * (Complex.abs z).log)
⊢ s1 * (Complex.abs (f' d c z) * (Complex.abs (f' d c z)).log)⁻¹ ≤
    s1 * ((b ^ (d - 1) - 1) * Complex.abs z * (Complex.abs z).log)⁻¹
Tactic:
refine mul_le_mul_of_nonneg_left (inv_le_inv_of_le (by positivity) ?_) s1p
Proof state after:
case refine_2
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
i b s0 s1 s2 : ℝ
c : ℂ
b3 : 3 ≤ b
s1p : 0 ≤ s1
s2p : 0 ≤ s2
bs0 : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s0 / (Complex.abs w * (Complex.abs w).log)
bs1 : ∀ {w : ℂ}, (b ^ (d - 1) - 1) * b ≤ Complex.abs w → f_error d w ≤ s1 / (Complex.abs w * (Complex.abs w).log)
b0' : 0 < b ^ (d - 1) - 1
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
b0 : 0 < b
z0 : 0 < Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 1 < (Complex.abs z).log
bb : ℝ
hbb : (b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1 = bb
b11 : 11 ≤ bb
bb3 : 3 ≤ bb * b
bs2 : ∀ {w : ℂ}, bb * b ≤ Complex.abs w → f_error d w ≤ s2 / (Complex.abs w * (Complex.abs w).log)
b0'' : 0 < 1 - (bb * b - 1)⁻¹
si : s0 + s1 / (b ^ (d - 1) - 1) + s2 / ((1 - (bb * b - 1)⁻¹) * bb) ≤ i
fz : Complex.abs z ^ d - Complex.abs c ≤ Complex.abs (f' d c z)
fz' : (b ^ (d - 1) - 1) * Complex.abs z ≤ Complex.abs (f' d c z)
zfz : Complex.abs z ≤ Complex.abs (f' d c z)
zffz : Complex.abs z ≤ Complex.abs (f' d c (f' d c z))
bfz : b ≤ Complex.abs (f' d c z)
ffz : bb * Complex.abs z ≤ Complex.abs (f' d c (f' d c z))
e0 : f_error d z ≤ s0 / (Complex.abs z * (Complex.abs z).log)
⊢ (b ^ (d - 1) - 1) * Complex.abs z * (Complex.abs z).log ≤ Complex.abs (f' d c z) * (Complex.abs (f' d c z)).log
Theorem: iter_error_le
Proof state before:
case refine_2
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
i b s0 s1 s2 : ℝ
c : ℂ
b3 : 3 ≤ b
s1p : 0 ≤ s1
s2p : 0 ≤ s2
bs0 : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s0 / (Complex.abs w * (Complex.abs w).log)
bs1 : ∀ {w : ℂ}, (b ^ (d - 1) - 1) * b ≤ Complex.abs w → f_error d w ≤ s1 / (Complex.abs w * (Complex.abs w).log)
b0' : 0 < b ^ (d - 1) - 1
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
b0 : 0 < b
z0 : 0 < Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 1 < (Complex.abs z).log
bb : ℝ
hbb : (b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1 = bb
b11 : 11 ≤ bb
bb3 : 3 ≤ bb * b
bs2 : ∀ {w : ℂ}, bb * b ≤ Complex.abs w → f_error d w ≤ s2 / (Complex.abs w * (Complex.abs w).log)
b0'' : 0 < 1 - (bb * b - 1)⁻¹
si : s0 + s1 / (b ^ (d - 1) - 1) + s2 / ((1 - (bb * b - 1)⁻¹) * bb) ≤ i
fz : Complex.abs z ^ d - Complex.abs c ≤ Complex.abs (f' d c z)
fz' : (b ^ (d - 1) - 1) * Complex.abs z ≤ Complex.abs (f' d c z)
zfz : Complex.abs z ≤ Complex.abs (f' d c z)
zffz : Complex.abs z ≤ Complex.abs (f' d c (f' d c z))
bfz : b ≤ Complex.abs (f' d c z)
ffz : bb * Complex.abs z ≤ Complex.abs (f' d c (f' d c z))
e0 : f_error d z ≤ s0 / (Complex.abs z * (Complex.abs z).log)
⊢ (b ^ (d - 1) - 1) * Complex.abs z * (Complex.abs z).log ≤ Complex.abs (f' d c z) * (Complex.abs (f' d c z)).log
Tactic:
exact mul_le_mul fz' (Real.log_le_log (by positivity) zfz) (by positivity)
  (le_trans b0.le bfz)
Proof state after:
no goals
Theorem: iter_error_le
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
i b s0 s1 s2 : ℝ
c : ℂ
b3 : 3 ≤ b
s1p : 0 ≤ s1
s2p : 0 ≤ s2
bs0 : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s0 / (Complex.abs w * (Complex.abs w).log)
bs1 : ∀ {w : ℂ}, (b ^ (d - 1) - 1) * b ≤ Complex.abs w → f_error d w ≤ s1 / (Complex.abs w * (Complex.abs w).log)
b0' : 0 < b ^ (d - 1) - 1
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
b0 : 0 < b
z0 : 0 < Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 1 < (Complex.abs z).log
bb : ℝ
hbb : (b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1 = bb
b11 : 11 ≤ bb
bb3 : 3 ≤ bb * b
bs2 : ∀ {w : ℂ}, bb * b ≤ Complex.abs w → f_error d w ≤ s2 / (Complex.abs w * (Complex.abs w).log)
b0'' : 0 < 1 - (bb * b - 1)⁻¹
si : s0 + s1 / (b ^ (d - 1) - 1) + s2 / ((1 - (bb * b - 1)⁻¹) * bb) ≤ i
fz : Complex.abs z ^ d - Complex.abs c ≤ Complex.abs (f' d c z)
fz' : (b ^ (d - 1) - 1) * Complex.abs z ≤ Complex.abs (f' d c z)
zfz : Complex.abs z ≤ Complex.abs (f' d c z)
zffz : Complex.abs z ≤ Complex.abs (f' d c (f' d c z))
bfz : b ≤ Complex.abs (f' d c z)
ffz : bb * Complex.abs z ≤ Complex.abs (f' d c (f' d c z))
e0 : f_error d z ≤ s0 / (Complex.abs z * (Complex.abs z).log)
⊢ 0 < (b ^ (d - 1) - 1) * Complex.abs z * (Complex.abs z).log
Tactic:
positivity
Proof state after:
no goals
Theorem: iter_error_le
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
i b s0 s1 s2 : ℝ
c : ℂ
b3 : 3 ≤ b
s1p : 0 ≤ s1
s2p : 0 ≤ s2
bs0 : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s0 / (Complex.abs w * (Complex.abs w).log)
bs1 : ∀ {w : ℂ}, (b ^ (d - 1) - 1) * b ≤ Complex.abs w → f_error d w ≤ s1 / (Complex.abs w * (Complex.abs w).log)
b0' : 0 < b ^ (d - 1) - 1
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
b0 : 0 < b
z0 : 0 < Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 1 < (Complex.abs z).log
bb : ℝ
hbb : (b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1 = bb
b11 : 11 ≤ bb
bb3 : 3 ≤ bb * b
bs2 : ∀ {w : ℂ}, bb * b ≤ Complex.abs w → f_error d w ≤ s2 / (Complex.abs w * (Complex.abs w).log)
b0'' : 0 < 1 - (bb * b - 1)⁻¹
si : s0 + s1 / (b ^ (d - 1) - 1) + s2 / ((1 - (bb * b - 1)⁻¹) * bb) ≤ i
fz : Complex.abs z ^ d - Complex.abs c ≤ Complex.abs (f' d c z)
fz' : (b ^ (d - 1) - 1) * Complex.abs z ≤ Complex.abs (f' d c z)
zfz : Complex.abs z ≤ Complex.abs (f' d c z)
zffz : Complex.abs z ≤ Complex.abs (f' d c (f' d c z))
bfz : b ≤ Complex.abs (f' d c z)
ffz : bb * Complex.abs z ≤ Complex.abs (f' d c (f' d c z))
e0 : f_error d z ≤ s0 / (Complex.abs z * (Complex.abs z).log)
⊢ 0 < Complex.abs z
Tactic:
positivity
Proof state after:
no goals