Theorems · Theorem · real analysis

Real.hasDerivAt_half_log_one_add_div_one_sub_sub_sum_range

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

Compute the derivative of the difference between $\frac{1}{2} * \log(\frac{1+x}{1-x})$ and its Taylor series at 0 up to order n. This is an auxiliary lemma for sum_range_sub_log_div_le and sum_range_le_log_div. Note that thanks to the geometric series, the derivative has a particularly simple form, and means that it is more convenient to avoid Taylor's theorem.

Defined in

Mathlib.Analysis.SpecialFunctions.Log.Deriv

Cited by

2 results in Mathlib

Foundations

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