English
As z→0, log(1+z) − logTaylor(n+1) z = O(z^{n+1}).
Русский
При z→0, log(1+z) − logTaylor(n+1) z = O(z^{n+1}).
LaTeX
$$$\\log(1+z) - \\mathrm{logTaylor}(n+1)\\,z = O(z^{n+1}) \\quad (z \\to 0)$$$
Lean4
/-- The limit of `x * log (1 + g x)` as `(x : ℝ) → ∞` is `t`,
where `t : ℂ` is the limit of `x * g x`. -/
theorem tendsto_mul_log_one_add_of_tendsto {g : ℝ → ℂ} {t : ℂ} (hg : Tendsto (fun x ↦ x * g x) atTop (𝓝 t)) :
Tendsto (fun x ↦ x * log (1 + g x)) atTop (𝓝 t) :=
by
apply hg.congr_dist
refine IsBigO.trans_tendsto ?_ tendsto_inv_atTop_zero.ofReal
simp_rw [dist_comm (_ * g _), dist_eq, ← mul_sub, isBigO_norm_left]
calc
_ =O[atTop] fun x ↦ x * g x ^ 2 :=
by
have hg0 :=
tendsto_zero_of_isBoundedUnder_smul_of_tendsto_cobounded hg.norm.isBoundedUnder_le
(RCLike.tendsto_ofReal_atTop_cobounded ℂ)
exact (isBigO_refl _ _).mul (log_sub_self_isBigO.comp_tendsto hg0)
_ =ᶠ[atTop] fun x ↦ (x * g x) ^ 2 * x⁻¹ :=
by
filter_upwards [eventually_ne_atTop 0] with x hx0
rw [ofReal_inv, eq_mul_inv_iff_mul_eq₀ (mod_cast hx0)]
ring
_ =O[atTop] _ := by simpa using isBigO_const_of_tendsto hg (one_ne_zero (α := ℂ)) |>.pow 2 |>.mul (isBigO_refl _ _)
