log_taylor_error_bound

proof body

Tactic-mode proof.

 108  -- Use the complex version and specialize to reals
 109  have hx_complex : ‖(x : ℂ)‖ < 1 := by rw [complex_norm_ofReal]; exact hx
 110  have h := Complex.norm_log_sub_logTaylor_le n hx_complex
 111  -- log(1 + x) for real x equals Re(log(1 + x)) when 1 + x > 0
 112  have h1x_pos : (0 : ℝ) < 1 + x := by
 113    have : -1 < x := by
 114      have := abs_lt.mp hx
 115      linarith
 116    linarith
 117  have hlog_real : log (1 + x) = (Complex.log (1 + x)).re := by
 118    have h1 : (1 : ℂ) + (x : ℂ) = ((1 + x : ℝ) : ℂ) := by push_cast; ring
 119    rw [h1, Complex.log_ofReal_re]
 120  rw [hlog_real]
 121  have hsub_re : (Complex.log (1 + ↑x) - Complex.logTaylor (n + 1) ↑x).re =
 122      (Complex.log (1 + ↑x)).re - (Complex.logTaylor (n + 1) ↑x).re := by
 123    simp only [Complex.sub_re]
 124  rw [← hsub_re]
 125  calc |((Complex.log (1 + ↑x) - Complex.logTaylor (n + 1) ↑x).re : ℝ)|
 126      ≤ ‖Complex.log (1 + ↑x) - Complex.logTaylor (n + 1) ↑x‖ := Complex.abs_re_le_norm _
 127    _ ≤ ‖(x : ℂ)‖ ^ (n + 1) * (1 - ‖(x : ℂ)‖)⁻¹ / (n + 1) := h
 128    _ = |x| ^ (n + 1) * (1 - |x|)⁻¹ / (n + 1) := by simp only [complex_norm_ofReal]
 129
 130/-- Key lemma: bound on log(1+y) using Mathlib's abs_log_sub_add_sum_range_le.
 131    For y > 0, log(1+y) = -log(1-(-y)), and the series is:
 132    log(1+y) = y - y²/2 + y³/3 - y⁴/4 + ...
 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-/