complex_norm_ofReal

formal source

  98  exact phi_sub_one_lt_one
  99
 100/-- Helper: ‖(x : ℂ)‖ = |x| for real x -/
 101lemma complex_norm_ofReal (x : ℝ) : ‖(x : ℂ)‖ = |x| := by
 102  have : (x : ℂ) = (RCLike.ofReal x : ℂ) := rfl
 103  rw [this, RCLike.norm_ofReal]
 104
 105/-- Error bound for log Taylor polynomial on reals, using Complex.norm_log_sub_logTaylor_le -/
 106lemma log_taylor_error_bound {x : ℝ} (hx : |x| < 1) (n : ℕ) :
 107    |log (1 + x) - (Complex.logTaylor (n + 1) x).re| ≤ |x| ^ (n + 1) * (1 - |x|)⁻¹ / (n + 1) := by
 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: