Theorem: iter_error_le (Ray/Dynamics/Multibrot/Iterates.lean)

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
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)

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)
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)

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)
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)

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)
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)

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
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)

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]
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)

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
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)

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
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)

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
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)

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
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)

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)
⊢ iter_error d c z ≤ i / (Complex.abs z * (Complex.abs z).log)
Tactic:
have ffz : bb * abs z ≤ abs (f' d c (f' d c z)) := by
  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]
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)
ffz : bb * 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)

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))
⊢ iter_error d c z ≤ i / (Complex.abs z * (Complex.abs z).log)
Tactic:
have e0 : f_error d z ≤ s0 / (abs z * log (abs z)) := bs0 bz
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)
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)
⊢ iter_error d c z ≤ i / (Complex.abs z * (Complex.abs z).log)

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)
e1 : f_error d (f' d c z) ≤ s1 / (b ^ (d - 1) - 1) / (Complex.abs z * (Complex.abs z).log)
e2 : iter_error d c (f' d c (f' d c z)) ≤ s2 / ((1 - (bb * b - 1)⁻¹) * bb) / (Complex.abs z * (Complex.abs z).log)
⊢ iter_error d c z ≤ i / (Complex.abs z * (Complex.abs z).log)
Tactic:
rw [iter_error_peel z3 cz, iter_error_peel (le_trans b3 bfz) (le_trans cz zfz), ←add_assoc]
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)
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)
e1 : f_error d (f' d c z) ≤ s1 / (b ^ (d - 1) - 1) / (Complex.abs z * (Complex.abs z).log)
e2 : iter_error d c (f' d c (f' d c z)) ≤ s2 / ((1 - (bb * b - 1)⁻¹) * bb) / (Complex.abs z * (Complex.abs z).log)
⊢ f_error d z + f_error d (f' d c z) + iter_error d c (f' d c (f' d c z)) ≤ i / (Complex.abs z * (Complex.abs z).log)

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)
e1 : f_error d (f' d c z) ≤ s1 / (b ^ (d - 1) - 1) / (Complex.abs z * (Complex.abs z).log)
e2 : iter_error d c (f' d c (f' d c z)) ≤ s2 / ((1 - (bb * b - 1)⁻¹) * bb) / (Complex.abs z * (Complex.abs z).log)
⊢ f_error d z + f_error d (f' d c z) + iter_error d c (f' d c (f' d c z)) ≤ i / (Complex.abs z * (Complex.abs z).log)
Tactic:
refine le_trans (add_le_add (add_le_add e0 e1) e2) ?_
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)
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)
e1 : f_error d (f' d c z) ≤ s1 / (b ^ (d - 1) - 1) / (Complex.abs z * (Complex.abs z).log)
e2 : iter_error d c (f' d c (f' d c z)) ≤ s2 / ((1 - (bb * b - 1)⁻¹) * bb) / (Complex.abs z * (Complex.abs z).log)
⊢ s0 / (Complex.abs z * (Complex.abs z).log) + s1 / (b ^ (d - 1) - 1) / (Complex.abs z * (Complex.abs z).log) +
      s2 / ((1 - (bb * b - 1)⁻¹) * bb) / (Complex.abs z * (Complex.abs z).log) ≤
    i / (Complex.abs z * (Complex.abs z).log)

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)
e1 : f_error d (f' d c z) ≤ s1 / (b ^ (d - 1) - 1) / (Complex.abs z * (Complex.abs z).log)
e2 : iter_error d c (f' d c (f' d c z)) ≤ s2 / ((1 - (bb * b - 1)⁻¹) * bb) / (Complex.abs z * (Complex.abs z).log)
⊢ s0 / (Complex.abs z * (Complex.abs z).log) + s1 / (b ^ (d - 1) - 1) / (Complex.abs z * (Complex.abs z).log) +
      s2 / ((1 - (bb * b - 1)⁻¹) * bb) / (Complex.abs z * (Complex.abs z).log) ≤
    i / (Complex.abs z * (Complex.abs z).log)
Tactic:
simp only [←add_div, le_refl]
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)
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)
e1 : f_error d (f' d c z) ≤ s1 / (b ^ (d - 1) - 1) / (Complex.abs z * (Complex.abs z).log)
e2 : iter_error d c (f' d c (f' d c z)) ≤ s2 / ((1 - (bb * b - 1)⁻¹) * bb) / (Complex.abs z * (Complex.abs z).log)
⊢ (s0 + s1 / (b ^ (d - 1) - 1) + s2 / ((1 - (bb * b - 1)⁻¹) * bb)) / (Complex.abs z * (Complex.abs z).log) ≤
    i / (Complex.abs z * (Complex.abs z).log)

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)
e1 : f_error d (f' d c z) ≤ s1 / (b ^ (d - 1) - 1) / (Complex.abs z * (Complex.abs z).log)
e2 : iter_error d c (f' d c (f' d c z)) ≤ s2 / ((1 - (bb * b - 1)⁻¹) * bb) / (Complex.abs z * (Complex.abs z).log)
⊢ (s0 + s1 / (b ^ (d - 1) - 1) + s2 / ((1 - (bb * b - 1)⁻¹) * bb)) / (Complex.abs z * (Complex.abs z).log) ≤
    i / (Complex.abs z * (Complex.abs z).log)
Tactic:
exact div_le_div_of_nonneg_right si (by positivity)
State after:
no goals

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
⊢ 0 < 3
Tactic:
norm_num
State after:
no goals

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
⊢ 0 < 3
Tactic:
norm_num
State after:
no goals

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
⊢ 3 ≤ 3
Tactic:
norm_num
State after:
no goals

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
⊢ 1 < 1.0986
Tactic:
norm_num
State after:
no goals

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
⊢ Complex.abs z ^ d - Complex.abs c ≤ Complex.abs (f' d c z)
Tactic:
calc abs (z^d + c)
  _ ≥ abs (z^d) - abs c := by bound
  _ = (abs z)^d - abs c := by rw [Complex.abs.map_pow]
State after:
no goals

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
⊢ Complex.abs (z ^ d + c) ≥ Complex.abs (z ^ d) - Complex.abs c
Tactic:
bound
State after:
no goals

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
⊢ Complex.abs (z ^ d) - Complex.abs c = Complex.abs z ^ d - Complex.abs c
Tactic:
rw [Complex.abs.map_pow]
State after:
no goals

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)
⊢ (b ^ (d - 1) - 1) * Complex.abs z ≤ Complex.abs (f' d c z)
Tactic:
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
State after:
no goals

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 - Complex.abs c ≥ Complex.abs z ^ d - Complex.abs z
Tactic:
bound
State after:
no goals

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 - Complex.abs z = Complex.abs z ^ (d - 1) * Complex.abs z - Complex.abs z
Tactic:
rw [←pow_succ, Nat.sub_add_cancel (d_ge_one d)]
State after:
no goals

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) * Complex.abs z - Complex.abs z = (Complex.abs z ^ (d - 1) - 1) * Complex.abs z
Tactic:
rw [sub_one_mul]
State after:
no goals

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
State after:
no goals

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]
State after:
no goals

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
State after:
no goals

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]
State after:
no goals

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
State after:
no goals

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)]
State after:
no goals

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
State after:
no goals

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]
State after:
no goals

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)
⊢ f_error d (f' d c z) ≤ s1 / (b ^ (d - 1) - 1) / (Complex.abs z * (Complex.abs z).log)
Tactic:
refine le_trans (bs1 ?_) ?_
State after:
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)

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)

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'
State after:
no goals

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)⁻¹]
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⁻¹

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]
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)⁻¹

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
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

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)
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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).log
Tactic:
positivity
State after:
no goals

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)
e1 : f_error d (f' d c z) ≤ s1 / (b ^ (d - 1) - 1) / (Complex.abs z * (Complex.abs z).log)
⊢ iter_error d c (f' d c (f' d c z)) ≤ s2 / ((1 - (bb * b - 1)⁻¹) * bb) / (Complex.abs z * (Complex.abs z).log)
Tactic:
refine le_trans (iter_error_weak d bb3 s2p bs2 ?_ (le_trans cz zffz)) ?_
State after:
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)
e1 : f_error d (f' d c z) ≤ s1 / (b ^ (d - 1) - 1) / (Complex.abs z * (Complex.abs z).log)
⊢ bb * b ≤ Complex.abs (f' d c (f' d c z))

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)
e1 : f_error d (f' d c z) ≤ s1 / (b ^ (d - 1) - 1) / (Complex.abs z * (Complex.abs z).log)
⊢ s2 / (1 - (bb * b - 1)⁻¹) / (Complex.abs (f' d c (f' d c z)) * (Complex.abs (f' d c (f' d c z))).log) ≤
    s2 / ((1 - (bb * b - 1)⁻¹) * bb) / (Complex.abs z * (Complex.abs z).log)

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)
e1 : f_error d (f' d c z) ≤ s1 / (b ^ (d - 1) - 1) / (Complex.abs z * (Complex.abs z).log)
⊢ bb * b ≤ Complex.abs (f' d c (f' d c z))
Tactic:
exact le_trans (mul_le_mul_of_nonneg_left bz (by positivity)) ffz
State after:
no goals

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)
e1 : f_error d (f' d c z) ≤ s1 / (b ^ (d - 1) - 1) / (Complex.abs z * (Complex.abs z).log)
⊢ 0 ≤ bb
Tactic:
positivity
State after:
no goals

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)
e1 : f_error d (f' d c z) ≤ s1 / (b ^ (d - 1) - 1) / (Complex.abs z * (Complex.abs z).log)
⊢ s2 / (1 - (bb * b - 1)⁻¹) / (Complex.abs (f' d c (f' d c z)) * (Complex.abs (f' d c (f' d c z))).log) ≤
    s2 / ((1 - (bb * b - 1)⁻¹) * bb) / (Complex.abs z * (Complex.abs z).log)
Tactic:
simp only [div_eq_mul_inv, mul_assoc s2]
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)
e1 : f_error d (f' d c z) ≤ s1 / (b ^ (d - 1) - 1) / (Complex.abs z * (Complex.abs z).log)
⊢ s2 * ((1 - (bb * b - 1)⁻¹)⁻¹ * (Complex.abs (f' d c (f' d c z)) * (Complex.abs (f' d c (f' d c z))).log)⁻¹) ≤
    s2 * (((1 - (bb * b - 1)⁻¹) * bb)⁻¹ * (Complex.abs z * (Complex.abs z).log)⁻¹)

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)
e1 : f_error d (f' d c z) ≤ s1 / (b ^ (d - 1) - 1) / (Complex.abs z * (Complex.abs z).log)
⊢ s2 * ((1 - (bb * b - 1)⁻¹)⁻¹ * (Complex.abs (f' d c (f' d c z)) * (Complex.abs (f' d c (f' d c z))).log)⁻¹) ≤
    s2 * (((1 - (bb * b - 1)⁻¹) * bb)⁻¹ * (Complex.abs z * (Complex.abs z).log)⁻¹)
Tactic:
refine mul_le_mul_of_nonneg_left ?_ s2p
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)
e1 : f_error d (f' d c z) ≤ s1 / (b ^ (d - 1) - 1) / (Complex.abs z * (Complex.abs z).log)
⊢ (1 - (bb * b - 1)⁻¹)⁻¹ * (Complex.abs (f' d c (f' d c z)) * (Complex.abs (f' d c (f' d c z))).log)⁻¹ ≤
    ((1 - (bb * b - 1)⁻¹) * bb)⁻¹ * (Complex.abs z * (Complex.abs z).log)⁻¹

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)
e1 : f_error d (f' d c z) ≤ s1 / (b ^ (d - 1) - 1) / (Complex.abs z * (Complex.abs z).log)
⊢ (1 - (bb * b - 1)⁻¹)⁻¹ * (Complex.abs (f' d c (f' d c z)) * (Complex.abs (f' d c (f' d c z))).log)⁻¹ ≤
    ((1 - (bb * b - 1)⁻¹) * bb)⁻¹ * (Complex.abs z * (Complex.abs z).log)⁻¹
Tactic:
simp only [←mul_inv, ←mul_assoc]
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)
e1 : f_error d (f' d c z) ≤ s1 / (b ^ (d - 1) - 1) / (Complex.abs z * (Complex.abs z).log)
⊢ ((1 - (bb * b - 1)⁻¹) * Complex.abs (f' d c (f' d c z)) * (Complex.abs (f' d c (f' d c z))).log)⁻¹ ≤
    ((1 - (bb * b - 1)⁻¹) * bb * Complex.abs z * (Complex.abs z).log)⁻¹

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)
e1 : f_error d (f' d c z) ≤ s1 / (b ^ (d - 1) - 1) / (Complex.abs z * (Complex.abs z).log)
⊢ ((1 - (bb * b - 1)⁻¹) * Complex.abs (f' d c (f' d c z)) * (Complex.abs (f' d c (f' d c z))).log)⁻¹ ≤
    ((1 - (bb * b - 1)⁻¹) * bb * Complex.abs z * (Complex.abs z).log)⁻¹
Tactic:
refine inv_le_inv_of_le (by positivity) ?_
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)
e1 : f_error d (f' d c z) ≤ s1 / (b ^ (d - 1) - 1) / (Complex.abs z * (Complex.abs z).log)
⊢ (1 - (bb * b - 1)⁻¹) * bb * Complex.abs z * (Complex.abs z).log ≤
    (1 - (bb * b - 1)⁻¹) * Complex.abs (f' d c (f' d c z)) * (Complex.abs (f' d c (f' d c z))).log

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)
e1 : f_error d (f' d c z) ≤ s1 / (b ^ (d - 1) - 1) / (Complex.abs z * (Complex.abs z).log)
⊢ (1 - (bb * b - 1)⁻¹) * bb * Complex.abs z * (Complex.abs z).log ≤
    (1 - (bb * b - 1)⁻¹) * Complex.abs (f' d c (f' d c z)) * (Complex.abs (f' d c (f' d c z))).log
Tactic:
refine mul_le_mul ?_ (Real.log_le_log z0 zffz) (by positivity) (by positivity)
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)
e1 : f_error d (f' d c z) ≤ s1 / (b ^ (d - 1) - 1) / (Complex.abs z * (Complex.abs z).log)
⊢ (1 - (bb * b - 1)⁻¹) * bb * Complex.abs z ≤ (1 - (bb * b - 1)⁻¹) * Complex.abs (f' d c (f' d c z))

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)
e1 : f_error d (f' d c z) ≤ s1 / (b ^ (d - 1) - 1) / (Complex.abs z * (Complex.abs z).log)
⊢ (1 - (bb * b - 1)⁻¹) * bb * Complex.abs z ≤ (1 - (bb * b - 1)⁻¹) * Complex.abs (f' d c (f' d c z))
Tactic:
rw [mul_assoc]
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)
e1 : f_error d (f' d c z) ≤ s1 / (b ^ (d - 1) - 1) / (Complex.abs z * (Complex.abs z).log)
⊢ (1 - (bb * b - 1)⁻¹) * (bb * Complex.abs z) ≤ (1 - (bb * b - 1)⁻¹) * Complex.abs (f' d c (f' d c z))

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)
e1 : f_error d (f' d c z) ≤ s1 / (b ^ (d - 1) - 1) / (Complex.abs z * (Complex.abs z).log)
⊢ (1 - (bb * b - 1)⁻¹) * (bb * Complex.abs z) ≤ (1 - (bb * b - 1)⁻¹) * Complex.abs (f' d c (f' d c z))
Tactic:
exact mul_le_mul_of_nonneg_left ffz (by positivity)
State after:
no goals

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)
e1 : f_error d (f' d c z) ≤ s1 / (b ^ (d - 1) - 1) / (Complex.abs z * (Complex.abs z).log)
⊢ 0 < (1 - (bb * b - 1)⁻¹) * bb * Complex.abs z * (Complex.abs z).log
Tactic:
positivity
State after:
no goals

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)
e1 : f_error d (f' d c z) ≤ s1 / (b ^ (d - 1) - 1) / (Complex.abs z * (Complex.abs z).log)
⊢ 0 ≤ (Complex.abs z).log
Tactic:
positivity
State after:
no goals

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)
e1 : f_error d (f' d c z) ≤ s1 / (b ^ (d - 1) - 1) / (Complex.abs z * (Complex.abs z).log)
⊢ 0 ≤ (1 - (bb * b - 1)⁻¹) * Complex.abs (f' d c (f' d c z))
Tactic:
positivity
State after:
no goals

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)
e1 : f_error d (f' d c z) ≤ s1 / (b ^ (d - 1) - 1) / (Complex.abs z * (Complex.abs z).log)
⊢ 0 ≤ 1 - (bb * b - 1)⁻¹
Tactic:
positivity
State after:
no goals

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)
e1 : f_error d (f' d c z) ≤ s1 / (b ^ (d - 1) - 1) / (Complex.abs z * (Complex.abs z).log)
e2 : iter_error d c (f' d c (f' d c z)) ≤ s2 / ((1 - (bb * b - 1)⁻¹) * bb) / (Complex.abs z * (Complex.abs z).log)
⊢ 0 ≤ Complex.abs z * (Complex.abs z).log
Tactic:
positivity
State after:
no goals