English
For any natural n and complex z with ||z||<1, the remainder of log(1+z) after its (n+1)-st Taylor polynomial is bounded by ||z||^{n+1}*(1-||z||)^{-1}/(n+1).
Русский
Для натурального n и комплексного z с ∥z∥<1 остаток разложения log(1+z) после (n+1)-й тейлеровой формулы ограничен величиной ∥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 of `log (1+z)` and its `(n+1)`st Taylor polynomial can be bounded in
terms of `‖z‖`. -/
theorem norm_log_sub_logTaylor_le (n : ℕ) {z : ℂ} (hz : ‖z‖ < 1) :
‖log (1 + z) - logTaylor (n + 1) z‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / (n + 1) :=
by
have help : IntervalIntegrable (fun t : ℝ ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1 :=
IntervalIntegrable.mul_const (Continuous.intervalIntegrable (by fun_prop) 0 1) (1 - ‖z‖)⁻¹
let f (z : ℂ) : ℂ := log (1 + z) - logTaylor (n + 1) z
let f' (z : ℂ) : ℂ := (-z) ^ n * (1 + z)⁻¹
have hderiv : ∀ t ∈ Set.Icc (0 : ℝ) 1, HasDerivAt f (f' (0 + t * z)) (0 + t * z) :=
by
intro t ht
rw [zero_add]
exact
hasDerivAt_log_sub_logTaylor n <|
StarConvex.add_smul_mem starConvex_one_slitPlane (mem_slitPlane_of_norm_lt_one hz) ht.1 ht.2
have hcont : ContinuousOn (fun t : ℝ ↦ f' (0 + t * z)) (Set.Icc 0 1) :=
by
simp only [zero_add]
exact (Continuous.continuousOn (by fun_prop)).mul <| continuousOn_one_add_mul_inv <| mem_slitPlane_of_norm_lt_one hz
have H : f z = z * ∫ t in (0 : ℝ)..1, (-(t * z)) ^ n * (1 + t * z)⁻¹ :=
by
convert (integral_unitInterval_deriv_eq_sub hcont hderiv).symm using 1
· simp only [f, zero_add, add_zero, log_one, logTaylor_at_zero, sub_self, sub_zero]
· simp only [f', real_smul, zero_add, smul_eq_mul]
unfold f at H
simp only [H, norm_mul]
simp_rw [neg_pow (_ * z) n, mul_assoc, intervalIntegral.integral_const_mul, mul_pow, mul_comm _ (z ^ n), mul_assoc,
intervalIntegral.integral_const_mul, norm_mul, norm_pow, norm_neg, norm_one, one_pow, one_mul, ← mul_assoc, ←
pow_succ', mul_div_assoc]
gcongr _ * ?_
calc
‖∫ t in (0 : ℝ)..1, (t : ℂ) ^ n * (1 + t * z)⁻¹‖
_ ≤ ∫ t in (0 : ℝ)..1, t ^ n * (1 - ‖z‖)⁻¹ :=
by
refine intervalIntegral.norm_integral_le_of_norm_le zero_le_one ?_ help
filter_upwards with t ⟨ht₀, ht₁⟩
rw [norm_mul, norm_pow, Complex.norm_of_nonneg ht₀.le]
gcongr
exact norm_one_add_mul_inv_le ⟨ht₀.le, ht₁⟩ hz
_ = (1 - ‖z‖)⁻¹ / (n + 1) :=
by
rw [intervalIntegral.integral_mul_const, mul_comm, integral_pow]
simp [field]
