Theorem: iter_error_le
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
i b s0 s1 s2 : ℝ
c : ℂ
b3 : 3 ≤ b
s1p : 0 ≤ s1
s2p : 0 ≤ s2
bs0 : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s0 / (Complex.abs w * (Complex.abs w).log)
bs1 : ∀ {w : ℂ}, (b ^ (d - 1) - 1) * b ≤ Complex.abs w → f_error d w ≤ s1 / (Complex.abs w * (Complex.abs w).log)
b0' : 0 < b ^ (d - 1) - 1
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
b0 : 0 < b
z0 : 0 < Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 1 < (Complex.abs z).log
bb : ℝ
hbb : (b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1 = bb
b11 : 11 ≤ bb
bb3 : 3 ≤ bb * b
bs2 : ∀ {w : ℂ}, bb * b ≤ Complex.abs w → f_error d w ≤ s2 / (Complex.abs w * (Complex.abs w).log)
b0'' : 0 < 1 - (bb * b - 1)⁻¹
si : s0 + s1 / (b ^ (d - 1) - 1) + s2 / ((1 - (bb * b - 1)⁻¹) * bb) ≤ i
fz : Complex.abs z ^ d - Complex.abs c ≤ Complex.abs (f' d c z)
fz' : (b ^ (d - 1) - 1) * Complex.abs z ≤ Complex.abs (f' d c z)
zfz : Complex.abs z ≤ Complex.abs (f' d c z)
zffz : Complex.abs z ≤ Complex.abs (f' d c (f' d c z))
bfz : b ≤ Complex.abs (f' d c z)
ffz : bb * Complex.abs z ≤ Complex.abs (f' d c (f' d c z))
e0 : f_error d z ≤ s0 / (Complex.abs z * (Complex.abs z).log)
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)) ?_
Proof 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)