ordinaryHypergeometric_eq_tsum — Mathlib

English

Equality of the hypergeometric-series with tsum form and the explicit coefficient form.

Русский

Эквивалентность гипергеометрической серии в форме суммы и в явной форме коэффициентов.

LaTeX

$$$$ ( ordinaryHypergeometricSeries( a,b,c) ).sum(x) = \\sum_{n\\ge0} coeff_n x^n $$$$

Lean4

theorem ordinaryHypergeometric_eq_tsum :
    ₂F₁ a b c = fun (x : 𝔸) =>
      ∑' n : ℕ,
        ((n !⁻¹ : 𝕂) * (ascPochhammer 𝕂 n).eval a * (ascPochhammer 𝕂 n).eval b * ((ascPochhammer 𝕂 n).eval c)⁻¹) •
          x ^ n :=
  funext (ordinaryHypergeometric_sum_eq a b c)

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