norm_log_one_add_sub_self_le — Mathlib

English

Same bound as above: for n ∈ Nat and z with ∥z∥<1, ∥log(1+z) − logTaylor(n+1) z∥ ≤ ∥z∥^{n+1}*(1-∥z∥)^{-1}/(n+1).

Русский

Та же граница остатка: для n ∈ Nat и z с ∥z∥<1, ∥log(1+z) − logTaylor(n+1) z∥ ≤ ∥z∥^{n+1}*(1-∥z∥)^{-1}/(n+1).

LaTeX

$$$\\displaystyle \\|\\log(1+z) - \\logTaylor(n+1)\\,z\\| \\le \\frac{\\|z\\|^{n+1}}{n+1}\\,(1 - \\|z\\|)^{-1}$$$

Lean4

/-- The difference `log (1+z) - z` is bounded by `‖z‖^2/(2*(1-‖z‖))` when `‖z‖ < 1`. -/
theorem norm_log_one_add_sub_self_le {z : ℂ} (hz : ‖z‖ < 1) : ‖log (1 + z) - z‖ ≤ ‖z‖ ^ 2 * (1 - ‖z‖)⁻¹ / 2 :=
  by
  convert norm_log_sub_logTaylor_le 1 hz using 2
  · simp [logTaylor_succ, logTaylor_zero, sub_eq_add_neg]
  · norm_num

Похожие утверждения