norm_log_one_sub_inv_add_logTaylor_neg_le

English

Bound the quantity log(1−z)^{-1} + logTaylor(n+1)(-z) by ∥z∥^{n+1}*(1−∥z∥)^{-1}/(n+1) for ∥z∥<1.

Русский

Для ∥z∥<1 ограничиваем выражение log(1−z)^{-1} + logTaylor(n+1)(−z) величиной ∥z∥^{n+1}*(1−∥z∥)^{-1}/(n+1).

LaTeX

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

Lean4

/-- The difference of `log (1-z)⁻¹` and its `(n+1)`st Taylor polynomial can be bounded in
terms of `‖z‖`. -/
theorem norm_log_one_sub_inv_add_logTaylor_neg_le (n : ℕ) {z : ℂ} (hz : ‖z‖ < 1) :
    ‖log (1 - z)⁻¹ + logTaylor (n + 1) (-z)‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / (n + 1) :=
  by
  rw [sub_eq_add_neg, log_inv _ <| slitPlane_arg_ne_pi <| mem_slitPlane_of_norm_lt_one <| (norm_neg z).symm ▸ hz, ←
    sub_neg_eq_add, ← neg_sub', norm_neg]
  convert norm_log_sub_logTaylor_le n <| (norm_neg z).symm ▸ hz using 4 <;> rw [norm_neg]

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