internlm/Lean-Github huggingface dataset:
Theorem: iter_error_weak_of_z33
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z33 : 33 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 3 ≤ 33
Tactic:
norm_num
Proof state after:
no goals
Theorem: iter_error_weak_of_z33
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z33 : 33 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 0 ≤ 0.512
Tactic:
norm_num
Proof state after:
no goals
Theorem: iter_error_weak_of_z33
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z33 : 33 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 0 < 1.0986
Tactic:
norm_num
Proof state after:
no goals
Theorem: iter_error_weak_of_z33
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z33 : 33 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
l0 : 0 < (Complex.abs z).log
⊢ 0.512 / (1 - (33 - 1)⁻¹) ≤ 0.529
Tactic:
norm_num
Proof state after:
no goals
Theorem: iter_error_weak_of_z33
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z33 : 33 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
l0 : 0 < (Complex.abs z).log
⊢ 0 ≤ 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)
bs2 :
  ∀ {w : ℂ},
    ((b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1) * b ≤ Complex.abs w →
      f_error d w ≤ s2 / (Complex.abs w * (Complex.abs w).log)
b11 : 11 ≤ (b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1
bb3 : 3 ≤ ((b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1) * b
b0' : 0 < b ^ (d - 1) - 1
b0'' : 0 < 1 - (((b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1) * b - 1)⁻¹
si :
  s0 + s1 / (b ^ (d - 1) - 1) +
      s2 / ((1 - (((b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1) * b - 1)⁻¹) * ((b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1)) ≤
    i
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ iter_error d c z ≤ i / (Complex.abs z * (Complex.abs z).log)
Tactic:
have b0 : 0 < b := lt_of_lt_of_le (by norm_num) b3
Proof state after:
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)
bs2 :
  ∀ {w : ℂ},
    ((b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1) * b ≤ Complex.abs w →
      f_error d w ≤ s2 / (Complex.abs w * (Complex.abs w).log)
b11 : 11 ≤ (b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1
bb3 : 3 ≤ ((b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1) * b
b0' : 0 < b ^ (d - 1) - 1
b0'' : 0 < 1 - (((b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1) * b - 1)⁻¹
si :
  s0 + s1 / (b ^ (d - 1) - 1) +
      s2 / ((1 - (((b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1) * b - 1)⁻¹) * ((b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1)) ≤
    i
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
b0 : 0 < b
⊢ iter_error d c z ≤ i / (Complex.abs z * (Complex.abs z).log)
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)
bs2 :
  ∀ {w : ℂ},
    ((b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1) * b ≤ Complex.abs w →
      f_error d w ≤ s2 / (Complex.abs w * (Complex.abs w).log)
b11 : 11 ≤ (b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1
bb3 : 3 ≤ ((b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1) * b
b0' : 0 < b ^ (d - 1) - 1
b0'' : 0 < 1 - (((b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1) * b - 1)⁻¹
si :
  s0 + s1 / (b ^ (d - 1) - 1) +
      s2 / ((1 - (((b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1) * b - 1)⁻¹) * ((b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1)) ≤
    i
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
b0 : 0 < b
⊢ iter_error d c z ≤ i / (Complex.abs z * (Complex.abs z).log)
Tactic:
have z0 : 0 < abs z := lt_of_lt_of_le (by norm_num) (le_trans b3 bz)
Proof state after:
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)
bs2 :
  ∀ {w : ℂ},
    ((b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1) * b ≤ Complex.abs w →
      f_error d w ≤ s2 / (Complex.abs w * (Complex.abs w).log)
b11 : 11 ≤ (b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1
bb3 : 3 ≤ ((b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1) * b
b0' : 0 < b ^ (d - 1) - 1
b0'' : 0 < 1 - (((b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1) * b - 1)⁻¹
si :
  s0 + s1 / (b ^ (d - 1) - 1) +
      s2 / ((1 - (((b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1) * b - 1)⁻¹) * ((b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1)) ≤
    i
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
b0 : 0 < b
z0 : 0 < Complex.abs z
⊢ iter_error d c z ≤ i / (Complex.abs z * (Complex.abs z).log)
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)
bs2 :
  ∀ {w : ℂ},
    ((b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1) * b ≤ Complex.abs w →
      f_error d w ≤ s2 / (Complex.abs w * (Complex.abs w).log)
b11 : 11 ≤ (b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1
bb3 : 3 ≤ ((b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1) * b
b0' : 0 < b ^ (d - 1) - 1
b0'' : 0 < 1 - (((b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1) * b - 1)⁻¹
si :
  s0 + s1 / (b ^ (d - 1) - 1) +
      s2 / ((1 - (((b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1) * b - 1)⁻¹) * ((b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1)) ≤
    i
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
b0 : 0 < b
z0 : 0 < Complex.abs z
⊢ iter_error d c z ≤ i / (Complex.abs z * (Complex.abs z).log)
Tactic:
have z3 : 3 ≤ abs z := le_trans (by norm_num) (le_trans b3 bz)
Proof state after:
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)
bs2 :
  ∀ {w : ℂ},
    ((b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1) * b ≤ Complex.abs w →
      f_error d w ≤ s2 / (Complex.abs w * (Complex.abs w).log)
b11 : 11 ≤ (b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1
bb3 : 3 ≤ ((b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1) * b
b0' : 0 < b ^ (d - 1) - 1
b0'' : 0 < 1 - (((b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1) * b - 1)⁻¹
si :
  s0 + s1 / (b ^ (d - 1) - 1) +
      s2 / ((1 - (((b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1) * b - 1)⁻¹) * ((b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1)) ≤
    i
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
⊢ iter_error d c z ≤ i / (Complex.abs z * (Complex.abs z).log)
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)
bs2 :
  ∀ {w : ℂ},
    ((b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1) * b ≤ Complex.abs w →
      f_error d w ≤ s2 / (Complex.abs w * (Complex.abs w).log)
b11 : 11 ≤ (b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1
bb3 : 3 ≤ ((b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1) * b
b0' : 0 < b ^ (d - 1) - 1
b0'' : 0 < 1 - (((b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1) * b - 1)⁻¹
si :
  s0 + s1 / (b ^ (d - 1) - 1) +
      s2 / ((1 - (((b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1) * b - 1)⁻¹) * ((b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1)) ≤
    i
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
⊢ iter_error d c z ≤ i / (Complex.abs z * (Complex.abs z).log)
Tactic:
have l0 : 1 < log (abs z) := lt_of_lt_of_le (by norm_num) (le_log_abs_z z3)
Proof state after:
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)
bs2 :
  ∀ {w : ℂ},
    ((b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1) * b ≤ Complex.abs w →
      f_error d w ≤ s2 / (Complex.abs w * (Complex.abs w).log)
b11 : 11 ≤ (b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1
bb3 : 3 ≤ ((b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1) * b
b0' : 0 < b ^ (d - 1) - 1
b0'' : 0 < 1 - (((b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1) * b - 1)⁻¹
si :
  s0 + s1 / (b ^ (d - 1) - 1) +
      s2 / ((1 - (((b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1) * b - 1)⁻¹) * ((b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1)) ≤
    i
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
⊢ iter_error d c z ≤ i / (Complex.abs z * (Complex.abs z).log)
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)
bs2 :
  ∀ {w : ℂ},
    ((b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1) * b ≤ Complex.abs w →
      f_error d w ≤ s2 / (Complex.abs w * (Complex.abs w).log)
b11 : 11 ≤ (b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1
bb3 : 3 ≤ ((b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1) * b
b0' : 0 < b ^ (d - 1) - 1
b0'' : 0 < 1 - (((b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1) * b - 1)⁻¹
si :
  s0 + s1 / (b ^ (d - 1) - 1) +
      s2 / ((1 - (((b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1) * b - 1)⁻¹) * ((b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1)) ≤
    i
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
⊢ iter_error d c z ≤ i / (Complex.abs z * (Complex.abs z).log)
Tactic:
generalize hbb : (b^(d-1)-1)^d * b^(d-1) - 1 = bb at b11 bb3 bs2 b0'' si
Proof state after:
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
⊢ iter_error d c z ≤ i / (Complex.abs z * (Complex.abs z).log)
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
⊢ iter_error d c z ≤ i / (Complex.abs z * (Complex.abs z).log)
Tactic:
have fz : (abs z)^d - abs c ≤ abs (f' d c z) := by
  calc abs (z^d + c)
    _ ≥ abs (z^d) - abs c := by bound
    _ = (abs z)^d - abs c := by rw [Complex.abs.map_pow]
Proof state after:
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)
⊢ iter_error d c z ≤ i / (Complex.abs z * (Complex.abs z).log)
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)
⊢ iter_error d c z ≤ i / (Complex.abs z * (Complex.abs z).log)
Tactic:
have fz' : (b^(d-1)-1) * abs z ≤ abs (f' d c z) := by
  calc abs (f' d c z)
    _ ≥ (abs z)^d - abs c := fz
    _ ≥ (abs z)^d - abs z := by bound
    _ = (abs z)^(d-1) * abs z - abs z := by rw [←pow_succ, Nat.sub_add_cancel (d_ge_one d)]
    _ = ((abs z)^(d-1) - 1) * abs z := by rw [sub_one_mul]
    _ ≥ (b^(d-1)-1) * abs z := by bound
Proof state after:
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)
⊢ iter_error d c z ≤ i / (Complex.abs z * (Complex.abs z).log)
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)
⊢ iter_error d c z ≤ i / (Complex.abs z * (Complex.abs z).log)
Tactic:
have zfz : abs z ≤ abs (f' d c z) := le_self_iter d z3 cz 1
Proof state after:
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)
⊢ iter_error d c z ≤ i / (Complex.abs z * (Complex.abs z).log)
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)
⊢ iter_error d c z ≤ i / (Complex.abs z * (Complex.abs z).log)
Tactic:
have zffz : abs z ≤ abs (f' d c (f' d c z)) := le_self_iter d z3 cz 2
Proof state after:
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))
⊢ iter_error d c z ≤ i / (Complex.abs z * (Complex.abs z).log)
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))
⊢ iter_error d c z ≤ i / (Complex.abs z * (Complex.abs z).log)
Tactic:
have bfz : b ≤ abs (f' d c z) := le_trans bz zfz
Proof state after:
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)
⊢ iter_error d c z ≤ i / (Complex.abs z * (Complex.abs z).log)