Theorems · Theorem · real analysis

Real.sum_range_le_log_div

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

For 0 ≤ x < 1, the partial sums of the series expansion of $\frac{1}{2} * \log(\frac{1+x}{1-x})$ at 0 form a lower bound for it. This shows that the absolute value in sum_range_sub_log_div_le can be dropped, and gives explicit lower bounds for logarithms.

Defined in

Mathlib.Analysis.SpecialFunctions.Log.Deriv

Cited by

1 results in Mathlib

Foundations

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