abs_log_sub_add_sum_range_le — Mathlib

English

For |x| < 1 and n ∈ ℕ, the remainder when approximating -log(1 - x) by the partial sum ∑_{i=0}^{n-1} x^{i+1}/(i+1) is bounded by |x|^{n+1}/(1 - |x|).

Русский

Для |x| < 1 и натурального n аппроксимация -log(1 - x) частичным суммированием ∑_{i=0}^{n-1} x^{i+1}/(i+1) имеет остаток по абсолютной величине, не превышающий |x|^{n+1}/(1 - |x|).

LaTeX

$$$\left| \sum_{i=0}^{n-1} \dfrac{x^{i+1}}{i+1} + \log(1 - x) \right| \le \dfrac{|x|^{n+1}}{1 - |x|}$$$

Lean4

/-- A crude lemma estimating the difference between `log (1-x)` and its Taylor series at `0`,
where the main point of the bound is that it tends to `0`. The goal is to deduce the series
expansion of the logarithm, in `hasSum_pow_div_log_of_abs_lt_1`.

TODO: use one of generic theorems about Taylor's series to prove this estimate.
-/
theorem abs_log_sub_add_sum_range_le {x : ℝ} (h : |x| < 1) (n : ℕ) :
    |(∑ i ∈ range n, x ^ (i + 1) / (i + 1)) + log (1 - x)| ≤ |x| ^ (n + 1) / (1 - |x|) := by
  /- For the proof, we show that the derivative of the function to be estimated is small,
      and then apply the mean value inequality. -/

  let F : ℝ → ℝ := fun x => (∑ i ∈ range n, x ^ (i + 1) / (i + 1)) + log (1 - x)
  let F' : ℝ → ℝ := fun x ↦
    -x ^ n /
      (1 - x)
        -- Porting note: In `mathlib3`, the proof used `deriv`/`DifferentiableAt`. `simp` failed to
          -- compute `deriv`, so I changed the proof to use `HasDerivAt` instead
          -- First step: compute the derivative of `F`

  have A : ∀ y ∈ Ioo (-1 : ℝ) 1, HasDerivAt F (F' y) y := fun y hy ↦
    by
    have : HasDerivAt F ((∑ i ∈ range n, ↑(i + 1) * y ^ i / (↑i + 1)) + (-1) / (1 - y)) y :=
      .add (.fun_sum fun i _ ↦ (hasDerivAt_pow (i + 1) y).div_const ((i : ℝ) + 1))
        (((hasDerivAt_id y).const_sub _).log <| sub_ne_zero.2 hy.2.ne')
    convert this using 1
    calc
      -y ^ n / (1 - y) = ∑ i ∈ Finset.range n, y ^ i + -1 / (1 - y) :=
        by
        simp [field, geom_sum_eq hy.2.ne, sub_ne_zero.2 hy.2.ne, sub_ne_zero.2 hy.2.ne']
        ring
      _ = ∑ i ∈ Finset.range n, ↑(i + 1) * y ^ i / (↑i + 1) + -1 / (1 - y) :=
        by
        congr with i
        rw [Nat.cast_succ, mul_div_cancel_left₀ _ (Nat.cast_add_one_pos i).ne']
          -- second step: show that the derivative of `F` is small

  have B : ∀ y ∈ Icc (-|x|) |x|, |F' y| ≤ |x| ^ n / (1 - |x|) := fun y hy ↦
    calc
      |F' y| = |y| ^ n / |1 - y| := by simp [F', abs_div]
      _ ≤ |x| ^ n / (1 - |x|) := by
        have : |y| ≤ |x| := abs_le.2 hy
        have : 1 - |x| ≤ |1 - y| := le_trans (by linarith [hy.2]) (le_abs_self _)
        gcongr
        exact sub_pos.2 h
  have C : ‖F x - F 0‖ ≤ |x| ^ n / (1 - |x|) * ‖x - 0‖ :=
    by
    refine
      Convex.norm_image_sub_le_of_norm_hasDerivWithin_le (fun y hy ↦ (A _ ?_).hasDerivWithinAt) B (convex_Icc _ _) ?_ ?_
    · exact Icc_subset_Ioo (neg_lt_neg h) h hy
    · simp
    ·
      simp [le_abs_self x, neg_le.mp (neg_le_abs x)]
        -- fourth step: conclude by massaging the inequality of the third step

  simpa [F, div_mul_eq_mul_div, pow_succ] using C

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