log_one_add_bounds

formal source

 133    The partial sum S_n = Σ_{i=0}^{n-1} (-1)^i * y^(i+1) / (i+1)
 134    Error bound: |log(1+y) - S_n| ≤ y^(n+1) / (1-y) for 0 < y < 1
 135-/
 136lemma log_one_add_bounds {y : ℝ} (hy_pos : 0 < y) (hy_lt : y < 1) (n : ℕ) :
 137    let S := ∑ i ∈ Finset.range n, (-1 : ℝ) ^ i * y ^ (i + 1) / (i + 1)
 138    let err := y ^ (n + 1) / (1 - y)
 139    S - err ≤ log (1 + y) ∧ log (1 + y) ≤ S + err := by
 140  intro S err
 141  -- Use abs_log_sub_add_sum_range_le with x = -y
 142  have hy_abs : |(-y)| < 1 := by simp [abs_of_neg (neg_neg_of_pos hy_pos)]; exact hy_lt
 143  have h := Real.abs_log_sub_add_sum_range_le hy_abs n
 144  -- The sum in Mathlib is Σ x^(i+1)/(i+1) = Σ (-y)^(i+1)/(i+1)
 145  -- = Σ (-1)^(i+1) * y^(i+1) / (i+1) = -S (since (-1)^(i+1) = -(-1)^i)
 146  have hsum_eq : (∑ i ∈ Finset.range n, (-y) ^ (i + 1) / (i + 1)) = -S := by
 147    simp only [S]
 148    rw [← Finset.sum_neg_distrib]
 149    congr 1
 150    ext i
 151    have : (-y) ^ (i + 1) = (-1) ^ (i + 1) * y ^ (i + 1) := by
 152      rw [neg_eq_neg_one_mul, mul_pow]
 153    rw [this]
 154    have h2 : (-1 : ℝ) ^ (i + 1) = -(-1 : ℝ) ^ i := by
 155      rw [pow_succ]
 156      ring
 157    rw [h2]
 158    ring
 159  -- log(1 - (-y)) = log(1 + y)
 160  have hlog_eq : log (1 - (-y)) = log (1 + y) := by ring_nf
 161  -- |(-y)| = y since y > 0
 162  have habs_neg_y : |(-y)| = y := by rw [abs_neg, abs_of_pos hy_pos]
 163  rw [hsum_eq, hlog_eq, habs_neg_y] at h
 164  -- h : |-S + log(1+y)| ≤ y^(n+1) / (1-y)
 165  -- i.e., |log(1+y) - S| ≤ err
 166  have h' : |log (1 + y) - S| ≤ err := by