hasSum_arctan — Mathlib

English

For |x| < 1, arctan x has a power series expansion ∑ (-1)^n x^{2n+1}/(2n+1) that sums to arctan x.

Русский

Для |x| < 1 имеет место степенной разложение arctan x: ∑_{n=0}^{∞} (-1)^n x^{2n+1}/(2n+1) = arctan x.

LaTeX

$$$$\\arctan x = \\sum_{n=0}^{\\infty} \\frac{(-1)^n x^{2n+1}}{2n+1}, \\quad |x| < 1.$$$$

Lean4

/-- The power series expansion of `Real.arctan`, valid on `-1 < x < 1`. -/
theorem hasSum_arctan {x : ℝ} (hx : ‖x‖ < 1) :
    HasSum (fun n : ℕ => (-1) ^ n * x ^ (2 * n + 1) / ↑(2 * n + 1)) (arctan x) :=
  mod_cast Complex.hasSum_arctan (z := x) (by simpa)

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