norm_log_one_sub_inv_sub_self_le — Mathlib

English

Bound the difference log(1−z)^{-1} − z by ∥z∥^2/(2(1−∥z∥)) for ∥z∥<1.

Русский

Ограничиваем разность log(1−z)^{-1} − z величиной ∥z∥^2/(2(1−∥z∥)) при ∥z∥<1.

LaTeX

$$$\\|\\log(1 - z)^{-1} - z\\| \\,\\le\\, \\frac{\\|z\\|^{2}}{2}\\,(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_sub_inv_sub_self_le {z : ℂ} (hz : ‖z‖ < 1) : ‖log (1 - z)⁻¹ - z‖ ≤ ‖z‖ ^ 2 * (1 - ‖z‖)⁻¹ / 2 :=
  by
  convert norm_log_one_sub_inv_add_logTaylor_neg_le 1 hz using 2
  · simp [logTaylor_succ, logTaylor_zero, sub_eq_add_neg]
  · norm_num

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