ordinaryHypergeometricSeries_apply_eq

English

The ordinary hypergeometric function equals the sum over n of its coefficient times x^n, with the sum taken in the usual sense (tsum).

Русский

Обыкновенная гипергеометрическая функция равна сумме по n коэффициента, умноженного на x^n.

LaTeX

$$$\\ordinaryHypergeometric(a,b,c) = \\sum_{n \\ge 0} (coeff_n) x^n$$$

Lean4

theorem ordinaryHypergeometricSeries_apply_eq (x : 𝔸) (n : ℕ) :
    (ordinaryHypergeometricSeries 𝔸 a b c n fun _ => x) =
      ((n !⁻¹ : 𝕂) * (ascPochhammer 𝕂 n).eval a * (ascPochhammer 𝕂 n).eval b * ((ascPochhammer 𝕂 n).eval c)⁻¹) •
        x ^ n :=
  by rw [ordinaryHypergeometricSeries, ofScalars_apply_eq]

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