Theorems · Theorem · real analysis

Real.abs_log_sub_add_sum_range_le

∀ {x : ℝ},
  |x| < 1 → ∀ (n : ℕ), |∑ i ∈ Finset.range n, x ^ (i + 1) / (↑i + 1) + Real.log (1 - x)| ≤ |x| ^ (n + 1) / (1 - |x|)

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.

Defined in

Mathlib.Analysis.SpecialFunctions.Log.Deriv

Cited by

4 results in Mathlib

Foundations

Depth 206 from the axioms · uses propext, Classical.choice, Quot.sound