internlm/Lean-Github huggingface dataset:
Theorem: f_error_le_of_z140
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z140 : 140 ≤ Complex.abs z
⊢ 73e-5 ≤ min 1 (((1.0004 - 1) * 2)⁻¹ + 1)⁻¹
Tactic:
norm_num
Proof state after:
no goals
Theorem: f_error_le_of_z140
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z140 : 140 ≤ Complex.abs z
⊢ 140⁻¹ ≤ min 1 (((1.004 - 1) * 2)⁻¹ + 1)⁻¹
Tactic:
norm_num
Proof state after:
no goals
Theorem: f_error_le_of_z140
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z140 : 140 ≤ Complex.abs z
⊢ 1 / 2 * 1.0004 * 1.004 ≤ 0.5023
Tactic:
norm_num
Proof state after:
no goals
Theorem: f_error_le_of_z140
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z140 : 140 ≤ Complex.abs z
⊢ 0 < 4.94
Tactic:
norm_num
Proof state after:
no goals
Theorem: f_error_le_of_z140
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z140 : 140 ≤ Complex.abs z
⊢ 1 < 1.0004
Tactic:
norm_num
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 ℕ
⊢ iter_error_sum d c z N ≤ s / (1 - (b - 1)⁻¹) / (Complex.abs z * (Complex.abs z).log)
Tactic:
have mf : ∀ k (w : ℂ), b ≤ abs w → abs c ≤ abs w → (b-1)^k * abs w ≤ abs ((f' d c)^[k] w) :=
  fun k w bw cw ↦ iter_large d b (by linarith) bw cw k
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)
⊢ iter_error_sum d c z N ≤ s / (1 - (b - 1)⁻¹) / (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)
⊢ iter_error_sum d c z N ≤ 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
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
⊢ iter_error_sum d c z N ≤ s / (1 - (b - 1)⁻¹) / (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
⊢ iter_error_sum d c z N ≤ 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
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
⊢ iter_error_sum d c z N ≤ s / (1 - (b - 1)⁻¹) / (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
⊢ iter_error_sum d c z N ≤ 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
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
⊢ iter_error_sum d c z N ≤ s / (1 - (b - 1)⁻¹) / (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
⊢ iter_error_sum d c z N ≤ s / (1 - (b - 1)⁻¹) / (Complex.abs z * (Complex.abs z).log)
Tactic:
have fb : ∀ k, f_error d ((f' d c)^[k] z) ≤ s / ((b-1)^k * abs z * log (abs z)) := by
  intro k
  have mk := mf k z bz cz
  have mk' : abs z ≤ abs ((f' d c)^[k] z) :=
    le_trans (le_mul_of_one_le_left (Complex.abs.nonneg _) (one_le_pow_of_one_le b1.le _)) mk
  refine le_trans (bs (le_trans bz mk')) ?_
  refine div_le_div_of_nonneg_left s0 (by positivity) ?_
  exact mul_le_mul mk (Real.log_le_log (by positivity) mk') l0.le (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
fb : ∀ (k : ℕ), f_error d ((f' d c)^[k] z) ≤ s / ((b - 1) ^ k * Complex.abs z * (Complex.abs z).log)
⊢ iter_error_sum d c z N ≤ s / (1 - (b - 1)⁻¹) / (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
fb : ∀ (k : ℕ), f_error d ((f' d c)^[k] z) ≤ s / ((b - 1) ^ k * Complex.abs z * (Complex.abs z).log)
⊢ iter_error_sum d c z N ≤ s / (1 - (b - 1)⁻¹) / (Complex.abs z * (Complex.abs z).log)
Tactic:
simp only [div_eq_mul_inv, ←mul_assoc, mul_inv, mul_comm _ ((b-1)^_)⁻¹,
  mul_comm _ (1-(b-1)⁻¹)⁻¹] at fb ⊢
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
fb : ∀ (k : ℕ), f_error d ((f' d c)^[k] z) ≤ ((b - 1) ^ k)⁻¹ * s * (Complex.abs z)⁻¹ * (Complex.abs z).log⁻¹
⊢ iter_error_sum d c z N ≤ (1 - (b - 1)⁻¹)⁻¹ * 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
fb : ∀ (k : ℕ), f_error d ((f' d c)^[k] z) ≤ ((b - 1) ^ k)⁻¹ * s * (Complex.abs z)⁻¹ * (Complex.abs z).log⁻¹
⊢ iter_error_sum d c z N ≤ (1 - (b - 1)⁻¹)⁻¹ * s * (Complex.abs z)⁻¹ * (Complex.abs z).log⁻¹
Tactic:
simp only [mul_assoc] at fb ⊢
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
fb : ∀ (k : ℕ), f_error d ((f' d c)^[k] z) ≤ ((b - 1) ^ k)⁻¹ * (s * ((Complex.abs z)⁻¹ * (Complex.abs z).log⁻¹))
⊢ iter_error_sum d c z N ≤ (1 - (b - 1)⁻¹)⁻¹ * (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
fb : ∀ (k : ℕ), f_error d ((f' d c)^[k] z) ≤ ((b - 1) ^ k)⁻¹ * (s * ((Complex.abs z)⁻¹ * (Complex.abs z).log⁻¹))
⊢ iter_error_sum d c z N ≤ (1 - (b - 1)⁻¹)⁻¹ * (s * ((Complex.abs z)⁻¹ * (Complex.abs z).log⁻¹))
Tactic:
generalize ht : s * ((Complex.abs z)⁻¹ * (log (Complex.abs z))⁻¹) = t at fb
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
⊢ iter_error_sum d c z N ≤ (1 - (b - 1)⁻¹)⁻¹ * t
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
⊢ iter_error_sum d c z N ≤ (1 - (b - 1)⁻¹)⁻¹ * t
Tactic:
have t0 : 0 ≤ t := by rw [←ht]; 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
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
t0 : 0 ≤ t
⊢ iter_error_sum d c z N ≤ (1 - (b - 1)⁻¹)⁻¹ * t
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
t0 : 0 ≤ t
⊢ iter_error_sum d c z N ≤ (1 - (b - 1)⁻¹)⁻¹ * t
Tactic:
apply le_trans (Finset.sum_le_sum (fun k _ ↦ fb k))
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
t0 : 0 ≤ t
⊢ (N.sum fun i => ((b - 1) ^ i)⁻¹ * t) ≤ (1 - (b - 1)⁻¹)⁻¹ * t
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
t0 : 0 ≤ t
⊢ (N.sum fun i => ((b - 1) ^ i)⁻¹ * t) ≤ (1 - (b - 1)⁻¹)⁻¹ * t
Tactic:
simp only [mul_comm _ t, ←Finset.mul_sum, ←inv_pow] at fb ⊢
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
t0 : 0 ≤ t
fb : ∀ (k : ℕ), f_error d ((f' d c)^[k] z) ≤ t * (b - 1)⁻¹ ^ k
⊢ (t * N.sum fun i => (b - 1)⁻¹ ^ i) ≤ t * (1 - (b - 1)⁻¹)⁻¹
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
⊢ (t * N.sum fun i => (b - 1)⁻¹ ^ i) ≤ t * (1 - (b - 1)⁻¹)⁻¹
Tactic:
exact mul_le_mul_of_nonneg_left (partial_geometric_bound _ (by positivity) (inv_lt_one b1)) t0
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 ℕ
k : ℕ
w : ℂ
bw : b ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
⊢ 2 ≤ b
Tactic:
linarith
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)
⊢ 3 ≤ Complex.abs z
Tactic:
linarith
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
⊢ 0 < 1.0986
Tactic:
norm_num
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
⊢ 1 < b - 1
Tactic:
linarith
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 : ℕ), f_error d ((f' d c)^[k] z) ≤ s / ((b - 1) ^ k * Complex.abs z * (Complex.abs z).log)
Tactic:
intro k
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 : ℕ
⊢ f_error d ((f' d c)^[k] z) ≤ 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 : ℕ
⊢ f_error d ((f' d c)^[k] z) ≤ s / ((b - 1) ^ k * Complex.abs z * (Complex.abs z).log)
Tactic:
have mk := mf k z bz cz
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)
⊢ f_error d ((f' d c)^[k] z) ≤ 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)
⊢ f_error d ((f' d c)^[k] z) ≤ s / ((b - 1) ^ k * Complex.abs z * (Complex.abs z).log)
Tactic:
have mk' : abs z ≤ abs ((f' d c)^[k] z) :=
  le_trans (le_mul_of_one_le_left (Complex.abs.nonneg _) (one_le_pow_of_one_le b1.le _)) 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)
⊢ f_error d ((f' d c)^[k] z) ≤ s / ((b - 1) ^ k * Complex.abs z * (Complex.abs z).log)