internlm/Lean-Github huggingface dataset:
Theorem: iter_error_sum_weak
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b s : ℝ
c : ℂ
b3 : 3 ≤ b
s0 : 0 ≤ s
bs : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s / (Complex.abs w * (Complex.abs w).log)
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
N : Finset ℕ
mf :
  ∀ (k : ℕ) (w : ℂ),
    b ≤ Complex.abs w → Complex.abs c ≤ Complex.abs w → (b - 1) ^ k * Complex.abs w ≤ Complex.abs ((f' d c)^[k] w)
z3 : 3 ≤ Complex.abs z
l0 : 0 < (Complex.abs z).log
b1 : 1 < b - 1
k : ℕ
mk : (b - 1) ^ k * Complex.abs z ≤ Complex.abs ((f' d c)^[k] z)
mk' : Complex.abs z ≤ Complex.abs ((f' d c)^[k] z)
⊢ f_error d ((f' d c)^[k] z) ≤ s / ((b - 1) ^ k * Complex.abs z * (Complex.abs z).log)
Tactic:
refine le_trans (bs (le_trans bz mk')) ?_
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b s : ℝ
c : ℂ
b3 : 3 ≤ b
s0 : 0 ≤ s
bs : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s / (Complex.abs w * (Complex.abs w).log)
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
N : Finset ℕ
mf :
  ∀ (k : ℕ) (w : ℂ),
    b ≤ Complex.abs w → Complex.abs c ≤ Complex.abs w → (b - 1) ^ k * Complex.abs w ≤ Complex.abs ((f' d c)^[k] w)
z3 : 3 ≤ Complex.abs z
l0 : 0 < (Complex.abs z).log
b1 : 1 < b - 1
k : ℕ
mk : (b - 1) ^ k * Complex.abs z ≤ Complex.abs ((f' d c)^[k] z)
mk' : Complex.abs z ≤ Complex.abs ((f' d c)^[k] z)
⊢ s / (Complex.abs ((f' d c)^[k] z) * (Complex.abs ((f' d c)^[k] z)).log) ≤
    s / ((b - 1) ^ k * Complex.abs z * (Complex.abs z).log)
Theorem: iter_error_sum_weak
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b s : ℝ
c : ℂ
b3 : 3 ≤ b
s0 : 0 ≤ s
bs : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s / (Complex.abs w * (Complex.abs w).log)
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
N : Finset ℕ
mf :
  ∀ (k : ℕ) (w : ℂ),
    b ≤ Complex.abs w → Complex.abs c ≤ Complex.abs w → (b - 1) ^ k * Complex.abs w ≤ Complex.abs ((f' d c)^[k] w)
z3 : 3 ≤ Complex.abs z
l0 : 0 < (Complex.abs z).log
b1 : 1 < b - 1
k : ℕ
mk : (b - 1) ^ k * Complex.abs z ≤ Complex.abs ((f' d c)^[k] z)
mk' : Complex.abs z ≤ Complex.abs ((f' d c)^[k] z)
⊢ s / (Complex.abs ((f' d c)^[k] z) * (Complex.abs ((f' d c)^[k] z)).log) ≤
    s / ((b - 1) ^ k * Complex.abs z * (Complex.abs z).log)
Tactic:
refine div_le_div_of_nonneg_left s0 (by positivity) ?_
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b s : ℝ
c : ℂ
b3 : 3 ≤ b
s0 : 0 ≤ s
bs : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s / (Complex.abs w * (Complex.abs w).log)
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
N : Finset ℕ
mf :
  ∀ (k : ℕ) (w : ℂ),
    b ≤ Complex.abs w → Complex.abs c ≤ Complex.abs w → (b - 1) ^ k * Complex.abs w ≤ Complex.abs ((f' d c)^[k] w)
z3 : 3 ≤ Complex.abs z
l0 : 0 < (Complex.abs z).log
b1 : 1 < b - 1
k : ℕ
mk : (b - 1) ^ k * Complex.abs z ≤ Complex.abs ((f' d c)^[k] z)
mk' : Complex.abs z ≤ Complex.abs ((f' d c)^[k] z)
⊢ (b - 1) ^ k * Complex.abs z * (Complex.abs z).log ≤ Complex.abs ((f' d c)^[k] z) * (Complex.abs ((f' d c)^[k] z)).log
Theorem: iter_error_sum_weak
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b s : ℝ
c : ℂ
b3 : 3 ≤ b
s0 : 0 ≤ s
bs : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s / (Complex.abs w * (Complex.abs w).log)
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
N : Finset ℕ
mf :
  ∀ (k : ℕ) (w : ℂ),
    b ≤ Complex.abs w → Complex.abs c ≤ Complex.abs w → (b - 1) ^ k * Complex.abs w ≤ Complex.abs ((f' d c)^[k] w)
z3 : 3 ≤ Complex.abs z
l0 : 0 < (Complex.abs z).log
b1 : 1 < b - 1
k : ℕ
mk : (b - 1) ^ k * Complex.abs z ≤ Complex.abs ((f' d c)^[k] z)
mk' : Complex.abs z ≤ Complex.abs ((f' d c)^[k] z)
⊢ (b - 1) ^ k * Complex.abs z * (Complex.abs z).log ≤ Complex.abs ((f' d c)^[k] z) * (Complex.abs ((f' d c)^[k] z)).log
Tactic:
exact mul_le_mul mk (Real.log_le_log (by positivity) mk') l0.le (by positivity)
Proof state after:
no goals
Theorem: iter_error_sum_weak
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b s : ℝ
c : ℂ
b3 : 3 ≤ b
s0 : 0 ≤ s
bs : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s / (Complex.abs w * (Complex.abs w).log)
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
N : Finset ℕ
mf :
  ∀ (k : ℕ) (w : ℂ),
    b ≤ Complex.abs w → Complex.abs c ≤ Complex.abs w → (b - 1) ^ k * Complex.abs w ≤ Complex.abs ((f' d c)^[k] w)
z3 : 3 ≤ Complex.abs z
l0 : 0 < (Complex.abs z).log
b1 : 1 < b - 1
k : ℕ
mk : (b - 1) ^ k * Complex.abs z ≤ Complex.abs ((f' d c)^[k] z)
mk' : Complex.abs z ≤ Complex.abs ((f' d c)^[k] z)
⊢ 0 < (b - 1) ^ k * Complex.abs z * (Complex.abs z).log
Tactic:
positivity
Proof state after:
no goals
Theorem: iter_error_sum_weak
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b s : ℝ
c : ℂ
b3 : 3 ≤ b
s0 : 0 ≤ s
bs : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s / (Complex.abs w * (Complex.abs w).log)
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
N : Finset ℕ
mf :
  ∀ (k : ℕ) (w : ℂ),
    b ≤ Complex.abs w → Complex.abs c ≤ Complex.abs w → (b - 1) ^ k * Complex.abs w ≤ Complex.abs ((f' d c)^[k] w)
z3 : 3 ≤ Complex.abs z
l0 : 0 < (Complex.abs z).log
b1 : 1 < b - 1
k : ℕ
mk : (b - 1) ^ k * Complex.abs z ≤ Complex.abs ((f' d c)^[k] z)
mk' : Complex.abs z ≤ Complex.abs ((f' d c)^[k] z)
⊢ 0 < Complex.abs z
Tactic:
positivity
Proof state after:
no goals
Theorem: iter_error_sum_weak
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b s : ℝ
c : ℂ
b3 : 3 ≤ b
s0 : 0 ≤ s
bs : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s / (Complex.abs w * (Complex.abs w).log)
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
N : Finset ℕ
mf :
  ∀ (k : ℕ) (w : ℂ),
    b ≤ Complex.abs w → Complex.abs c ≤ Complex.abs w → (b - 1) ^ k * Complex.abs w ≤ Complex.abs ((f' d c)^[k] w)
z3 : 3 ≤ Complex.abs z
l0 : 0 < (Complex.abs z).log
b1 : 1 < b - 1
k : ℕ
mk : (b - 1) ^ k * Complex.abs z ≤ Complex.abs ((f' d c)^[k] z)
mk' : Complex.abs z ≤ Complex.abs ((f' d c)^[k] z)
⊢ 0 ≤ Complex.abs ((f' d c)^[k] z)
Tactic:
positivity
Proof state after:
no goals
Theorem: iter_error_sum_weak
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b s : ℝ
c : ℂ
b3 : 3 ≤ b
s0 : 0 ≤ s
bs : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s / (Complex.abs w * (Complex.abs w).log)
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
N : Finset ℕ
mf :
  ∀ (k : ℕ) (w : ℂ),
    b ≤ Complex.abs w → Complex.abs c ≤ Complex.abs w → (b - 1) ^ k * Complex.abs w ≤ Complex.abs ((f' d c)^[k] w)
z3 : 3 ≤ Complex.abs z
l0 : 0 < (Complex.abs z).log
b1 : 1 < b - 1
t : ℝ
ht : s * ((Complex.abs z)⁻¹ * (Complex.abs z).log⁻¹) = t
fb : ∀ (k : ℕ), f_error d ((f' d c)^[k] z) ≤ ((b - 1) ^ k)⁻¹ * t
⊢ 0 ≤ t
Tactic:
rw [←ht]
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b s : ℝ
c : ℂ
b3 : 3 ≤ b
s0 : 0 ≤ s
bs : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s / (Complex.abs w * (Complex.abs w).log)
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
N : Finset ℕ
mf :
  ∀ (k : ℕ) (w : ℂ),
    b ≤ Complex.abs w → Complex.abs c ≤ Complex.abs w → (b - 1) ^ k * Complex.abs w ≤ Complex.abs ((f' d c)^[k] w)
z3 : 3 ≤ Complex.abs z
l0 : 0 < (Complex.abs z).log
b1 : 1 < b - 1
t : ℝ
ht : s * ((Complex.abs z)⁻¹ * (Complex.abs z).log⁻¹) = t
fb : ∀ (k : ℕ), f_error d ((f' d c)^[k] z) ≤ ((b - 1) ^ k)⁻¹ * t
⊢ 0 ≤ s * ((Complex.abs z)⁻¹ * (Complex.abs z).log⁻¹)
Theorem: iter_error_sum_weak
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b s : ℝ
c : ℂ
b3 : 3 ≤ b
s0 : 0 ≤ s
bs : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s / (Complex.abs w * (Complex.abs w).log)
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
N : Finset ℕ
mf :
  ∀ (k : ℕ) (w : ℂ),
    b ≤ Complex.abs w → Complex.abs c ≤ Complex.abs w → (b - 1) ^ k * Complex.abs w ≤ Complex.abs ((f' d c)^[k] w)
z3 : 3 ≤ Complex.abs z
l0 : 0 < (Complex.abs z).log
b1 : 1 < b - 1
t : ℝ
ht : s * ((Complex.abs z)⁻¹ * (Complex.abs z).log⁻¹) = t
fb : ∀ (k : ℕ), f_error d ((f' d c)^[k] z) ≤ ((b - 1) ^ k)⁻¹ * t
⊢ 0 ≤ s * ((Complex.abs z)⁻¹ * (Complex.abs z).log⁻¹)
Tactic:
positivity
Proof state after:
no goals
Theorem: iter_error_sum_weak
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b s : ℝ
c : ℂ
b3 : 3 ≤ b
s0 : 0 ≤ s
bs : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s / (Complex.abs w * (Complex.abs w).log)
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
N : Finset ℕ
mf :
  ∀ (k : ℕ) (w : ℂ),
    b ≤ Complex.abs w → Complex.abs c ≤ Complex.abs w → (b - 1) ^ k * Complex.abs w ≤ Complex.abs ((f' d c)^[k] w)
z3 : 3 ≤ Complex.abs z
l0 : 0 < (Complex.abs z).log
b1 : 1 < b - 1
t : ℝ
ht : s * ((Complex.abs z)⁻¹ * (Complex.abs z).log⁻¹) = t
t0 : 0 ≤ t
fb : ∀ (k : ℕ), f_error d ((f' d c)^[k] z) ≤ t * (b - 1)⁻¹ ^ k
⊢ 0 ≤ (b - 1)⁻¹
Tactic:
positivity
Proof state after:
no goals
Theorem: iter_error_summable
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ Summable fun n => f_error d ((f' d c)^[n] z)
Tactic:
apply summable_of_sum_le
Proof state after:
case hf
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 0 ≤ fun n => f_error d ((f' d c)^[n] z)

case h
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ ∀ (u : Finset ℕ), (u.sum fun x => f_error d ((f' d c)^[x] z)) ≤ ?c

case c
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ ℝ
Theorem: iter_error_summable
Proof state before:
case hf
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 0 ≤ fun n => f_error d ((f' d c)^[n] z)
Tactic:
intro n
Proof state after:
case hf
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
⊢ 0 n ≤ (fun n => f_error d ((f' d c)^[n] z)) n
Theorem: iter_error_summable
Proof state before:
case hf
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
⊢ 0 n ≤ (fun n => f_error d ((f' d c)^[n] z)) n
Tactic:
exact f_error_nonneg (le_trans z3 (le_self_iter d z3 cz n))
Proof state after:
no goals
Theorem: iter_error_summable
Proof state before:
case h
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ ∀ (u : Finset ℕ), (u.sum fun x => f_error d ((f' d c)^[x] z)) ≤ ?c
Tactic:
intro N
Proof state after:
case h
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
N : Finset ℕ
⊢ (N.sum fun x => f_error d ((f' d c)^[x] z)) ≤ ?c
Theorem: iter_error_summable
Proof state before:
case h
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
N : Finset ℕ
⊢ (N.sum fun x => f_error d ((f' d c)^[x] z)) ≤ ?c
Tactic:
exact iter_error_sum_weak d (le_refl _) (by norm_num) (f_error_le_of_z3 d) z3 cz
Proof state after:
no goals
Theorem: iter_error_summable
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
N : Finset ℕ
⊢ 0 ≤ 0.699
Tactic:
norm_num
Proof state after:
no goals
Theorem: iter_error_peel
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ iter_error d c z = f_error d z + iter_error d c (f' d c z)
Tactic:
have h0 := sum_drop (iter_error_summable d z3 cz).hasSum
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
h0 :
  HasSum (fun n => f_error d ((f' d c)^[n + 1] z)) (∑' (b : ℕ), f_error d ((f' d c)^[b] z) - f_error d ((f' d c)^[0] z))
⊢ iter_error d c z = f_error d z + iter_error d c (f' d c z)
Theorem: iter_error_peel
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
h0 :
  HasSum (fun n => f_error d ((f' d c)^[n + 1] z)) (∑' (b : ℕ), f_error d ((f' d c)^[b] z) - f_error d ((f' d c)^[0] z))
⊢ iter_error d c z = f_error d z + iter_error d c (f' d c z)
Tactic:
simp only [Function.iterate_succ_apply, zero_add, Function.iterate_zero, id_eq] at h0
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
h0 : HasSum (fun n => f_error d ((f' d c)^[n] (f' d c z))) (∑' (b : ℕ), f_error d ((f' d c)^[b] z) - f_error d z)
⊢ iter_error d c z = f_error d z + iter_error d c (f' d c z)
Theorem: iter_error_peel
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
h0 : HasSum (fun n => f_error d ((f' d c)^[n] (f' d c z))) (∑' (b : ℕ), f_error d ((f' d c)^[b] z) - f_error d z)
⊢ iter_error d c z = f_error d z + iter_error d c (f' d c z)
Tactic:
simp only [iter_error, h0.tsum_eq]
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
h0 : HasSum (fun n => f_error d ((f' d c)^[n] (f' d c z))) (∑' (b : ℕ), f_error d ((f' d c)^[b] z) - f_error d z)
⊢ ∑' (n : ℕ), f_error d ((f' d c)^[n] z) = f_error d z + (∑' (n : ℕ), f_error d ((f' d c)^[n] z) - f_error d z)
Theorem: iter_error_peel
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
h0 : HasSum (fun n => f_error d ((f' d c)^[n] (f' d c z))) (∑' (b : ℕ), f_error d ((f' d c)^[b] z) - f_error d z)
⊢ ∑' (n : ℕ), f_error d ((f' d c)^[n] z) = f_error d z + (∑' (n : ℕ), f_error d ((f' d c)^[n] z) - f_error d z)
Tactic:
abel
Proof state after:
no goals
Theorem: iter_error_weak
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b s : ℝ
c : ℂ
b3 : 3 ≤ b
s0 : 0 ≤ s
bs : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s / (Complex.abs w * (Complex.abs w).log)
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ iter_error d c z ≤ s / (1 - (b - 1)⁻¹) / (Complex.abs z * (Complex.abs z).log)
Tactic:
have z3 : 3 ≤ abs z := by linarith
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b s : ℝ
c : ℂ
b3 : 3 ≤ b
s0 : 0 ≤ s
bs : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s / (Complex.abs w * (Complex.abs w).log)
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
⊢ iter_error d c z ≤ s / (1 - (b - 1)⁻¹) / (Complex.abs z * (Complex.abs z).log)
Theorem: iter_error_weak
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b s : ℝ
c : ℂ
b3 : 3 ≤ b
s0 : 0 ≤ s
bs : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s / (Complex.abs w * (Complex.abs w).log)
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
⊢ iter_error d c z ≤ s / (1 - (b - 1)⁻¹) / (Complex.abs z * (Complex.abs z).log)
Tactic:
have l0 : 0 < log (abs z) := lt_of_lt_of_le (by norm_num) (le_log_abs_z z3)
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b s : ℝ
c : ℂ
b3 : 3 ≤ b
s0 : 0 ≤ s
bs : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s / (Complex.abs w * (Complex.abs w).log)
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 0 < (Complex.abs z).log
⊢ iter_error d c z ≤ s / (1 - (b - 1)⁻¹) / (Complex.abs z * (Complex.abs z).log)
Theorem: iter_error_weak
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b s : ℝ
c : ℂ
b3 : 3 ≤ b
s0 : 0 ≤ s
bs : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s / (Complex.abs w * (Complex.abs w).log)
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 0 < (Complex.abs z).log
⊢ iter_error d c z ≤ s / (1 - (b - 1)⁻¹) / (Complex.abs z * (Complex.abs z).log)
Tactic:
have b1 : 1 < b - 1 := by linarith
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b s : ℝ
c : ℂ
b3 : 3 ≤ b
s0 : 0 ≤ s
bs : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s / (Complex.abs w * (Complex.abs w).log)
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 0 < (Complex.abs z).log
b1 : 1 < b - 1
⊢ iter_error d c z ≤ s / (1 - (b - 1)⁻¹) / (Complex.abs z * (Complex.abs z).log)
Theorem: iter_error_weak
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b s : ℝ
c : ℂ
b3 : 3 ≤ b
s0 : 0 ≤ s
bs : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s / (Complex.abs w * (Complex.abs w).log)
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 0 < (Complex.abs z).log
b1 : 1 < b - 1
⊢ iter_error d c z ≤ s / (1 - (b - 1)⁻¹) / (Complex.abs z * (Complex.abs z).log)
Tactic:
have b0 : 0 ≤ 1 - (b - 1)⁻¹ := sub_nonneg.mpr (inv_le_one b1.le)
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b s : ℝ
c : ℂ
b3 : 3 ≤ b
s0 : 0 ≤ s
bs : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s / (Complex.abs w * (Complex.abs w).log)
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 0 < (Complex.abs z).log
b1 : 1 < b - 1
b0 : 0 ≤ 1 - (b - 1)⁻¹
⊢ iter_error d c z ≤ s / (1 - (b - 1)⁻¹) / (Complex.abs z * (Complex.abs z).log)
Theorem: iter_error_weak
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b s : ℝ
c : ℂ
b3 : 3 ≤ b
s0 : 0 ≤ s
bs : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s / (Complex.abs w * (Complex.abs w).log)
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 0 < (Complex.abs z).log
b1 : 1 < b - 1
b0 : 0 ≤ 1 - (b - 1)⁻¹
⊢ iter_error d c z ≤ s / (1 - (b - 1)⁻¹) / (Complex.abs z * (Complex.abs z).log)
Tactic:
refine tsum_le_of_sum_le' ?_ ?_
Proof state after:
case refine_1
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b s : ℝ
c : ℂ
b3 : 3 ≤ b
s0 : 0 ≤ s
bs : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s / (Complex.abs w * (Complex.abs w).log)
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 0 < (Complex.abs z).log
b1 : 1 < b - 1
b0 : 0 ≤ 1 - (b - 1)⁻¹
⊢ 0 ≤ s / (1 - (b - 1)⁻¹) / (Complex.abs z * (Complex.abs z).log)

case refine_2
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b s : ℝ
c : ℂ
b3 : 3 ≤ b
s0 : 0 ≤ s
bs : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s / (Complex.abs w * (Complex.abs w).log)
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 0 < (Complex.abs z).log
b1 : 1 < b - 1
b0 : 0 ≤ 1 - (b - 1)⁻¹
⊢ ∀ (s_1 : Finset ℕ),
    (s_1.sum fun i => f_error d ((f' d c)^[i] z)) ≤ s / (1 - (b - 1)⁻¹) / (Complex.abs z * (Complex.abs z).log)
Theorem: iter_error_weak
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b s : ℝ
c : ℂ
b3 : 3 ≤ b
s0 : 0 ≤ s
bs : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s / (Complex.abs w * (Complex.abs w).log)
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 3 ≤ Complex.abs z
Tactic:
linarith
Proof state after:
no goals
Theorem: iter_error_weak
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b s : ℝ
c : ℂ
b3 : 3 ≤ b
s0 : 0 ≤ s
bs : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s / (Complex.abs w * (Complex.abs w).log)
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
⊢ 0 < 1.0986
Tactic:
norm_num
Proof state after:
no goals
Theorem: iter_error_weak
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b s : ℝ
c : ℂ
b3 : 3 ≤ b
s0 : 0 ≤ s
bs : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s / (Complex.abs w * (Complex.abs w).log)
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 0 < (Complex.abs z).log
⊢ 1 < b - 1
Tactic:
linarith
Proof state after:
no goals
Theorem: iter_error_weak
Proof state before:
case refine_1
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b s : ℝ
c : ℂ
b3 : 3 ≤ b
s0 : 0 ≤ s
bs : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s / (Complex.abs w * (Complex.abs w).log)
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 0 < (Complex.abs z).log
b1 : 1 < b - 1
b0 : 0 ≤ 1 - (b - 1)⁻¹
⊢ 0 ≤ s / (1 - (b - 1)⁻¹) / (Complex.abs z * (Complex.abs z).log)
Tactic:
positivity
Proof state after:
no goals
Theorem: iter_error_weak
Proof state before:
case refine_2
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b s : ℝ
c : ℂ
b3 : 3 ≤ b
s0 : 0 ≤ s
bs : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s / (Complex.abs w * (Complex.abs w).log)
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 0 < (Complex.abs z).log
b1 : 1 < b - 1
b0 : 0 ≤ 1 - (b - 1)⁻¹
⊢ ∀ (s_1 : Finset ℕ),
    (s_1.sum fun i => f_error d ((f' d c)^[i] z)) ≤ s / (1 - (b - 1)⁻¹) / (Complex.abs z * (Complex.abs z).log)
Tactic:
intro N
Proof state after:
case refine_2
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b s : ℝ
c : ℂ
b3 : 3 ≤ b
s0 : 0 ≤ s
bs : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s / (Complex.abs w * (Complex.abs w).log)
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 0 < (Complex.abs z).log
b1 : 1 < b - 1
b0 : 0 ≤ 1 - (b - 1)⁻¹
N : Finset ℕ
⊢ (N.sum fun i => f_error d ((f' d c)^[i] z)) ≤ s / (1 - (b - 1)⁻¹) / (Complex.abs z * (Complex.abs z).log)
Theorem: iter_error_weak
Proof state before:
case refine_2
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b s : ℝ
c : ℂ
b3 : 3 ≤ b
s0 : 0 ≤ s
bs : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s / (Complex.abs w * (Complex.abs w).log)
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 0 < (Complex.abs z).log
b1 : 1 < b - 1
b0 : 0 ≤ 1 - (b - 1)⁻¹
N : Finset ℕ
⊢ (N.sum fun i => f_error d ((f' d c)^[i] z)) ≤ s / (1 - (b - 1)⁻¹) / (Complex.abs z * (Complex.abs z).log)
Tactic:
exact iter_error_sum_weak d b3 s0 bs bz cz
Proof state after:
no goals
Theorem: iter_error_weak_of_z33
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z33 : 33 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ iter_error d c z ≤ 0.529 / (Complex.abs z * (Complex.abs z).log)
Tactic:
refine le_trans (iter_error_weak d (b := 33) (by norm_num) (by norm_num)
  (fun {_} bz ↦ f_error_le_of_z33 d bz) z33 cz) ?_
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z33 : 33 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 0.512 / (1 - (33 - 1)⁻¹) / (Complex.abs z * (Complex.abs z).log) ≤ 0.529 / (Complex.abs z * (Complex.abs z).log)
Theorem: iter_error_weak_of_z33
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z33 : 33 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 0.512 / (1 - (33 - 1)⁻¹) / (Complex.abs z * (Complex.abs z).log) ≤ 0.529 / (Complex.abs z * (Complex.abs z).log)
Tactic:
have l0 : 0 < log (abs z) :=
  lt_of_lt_of_le (by norm_num) (le_log_abs_z (le_trans (by norm_num) z33))
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z33 : 33 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
l0 : 0 < (Complex.abs z).log
⊢ 0.512 / (1 - (33 - 1)⁻¹) / (Complex.abs z * (Complex.abs z).log) ≤ 0.529 / (Complex.abs z * (Complex.abs z).log)
Theorem: iter_error_weak_of_z33
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z33 : 33 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
l0 : 0 < (Complex.abs z).log
⊢ 0.512 / (1 - (33 - 1)⁻¹) / (Complex.abs z * (Complex.abs z).log) ≤ 0.529 / (Complex.abs z * (Complex.abs z).log)
Tactic:
exact div_le_div_of_nonneg_right (by norm_num) (by positivity)
Proof state after:
no goals