log_one_add_bounds

proof body

Tactic-mode proof.

 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
 167    have heq : -S + log (1 + y) = log (1 + y) - S := by ring
 168    rw [heq] at h
 169    exact h
 170  constructor
 171  · -- S - err ≤ log(1+y)
 172    have := neg_abs_le (log (1 + y) - S)
 173    linarith [h']
 174  · -- log(1+y) ≤ S + err
 175    have := le_abs_self (log (1 + y) - S)
 176    linarith [h']
 177
 178/-- Taylor sum for exp at x = 48/100 (rational) -/