log_sub_logTaylor_isBigO — Mathlib

English

For any natural n and complex z, the remainder log(1+z) − logTaylor(n+1) z is O(z^{n+1}) as z→0.

Русский

Остаток log(1+z) − logTaylor(n+1) z равен O(z^{n+1}) при z → 0.

LaTeX

$$$\\log(1+z) - \\mathrm{logTaylor}(n+1)\\,z =O(z^{n+1})\\quad \\text{при } z \\to 0$$$

Lean4

theorem log_sub_logTaylor_isBigO (n : ℕ) : (fun z ↦ log (1 + z) - logTaylor (n + 1) z) =O[𝓝 0] fun z ↦ z ^ (n + 1) :=
  by
  rw [Asymptotics.isBigO_iff]
  use 2 / (n + 1)
  filter_upwards [eventually_norm_sub_lt 0 one_pos, eventually_norm_sub_lt 0 (show 0 < 1 / 2 by simp)] with z hz1 hz12
  rw [sub_zero] at hz1 hz12
  have : (1 - ‖z‖)⁻¹ ≤ 2 := by rw [inv_le_comm₀ (sub_pos_of_lt hz1) two_pos]; linarith
  apply (norm_log_sub_logTaylor_le n hz1).trans
  rw [mul_div_assoc, mul_comm, norm_pow]
  gcongr

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