ordinaryHypergeometricSeries_apply_eq'

English

Equality of the hypergeometric expression with tsum over n of its nth term.

Русский

Эквивалентность гипергеометрического выражения и суммы по n.

LaTeX

$$$\\text{ordinaryHypergeometric}(a,b,c) = \\operatorname{tsum}_{n\\ge0} coeff_n x^n$$$

Lean4

/-- This naming follows the convention of `NormedSpace.expSeries_apply_eq'`. -/
theorem ordinaryHypergeometricSeries_apply_eq' (x : 𝔸) :
    (fun n => ordinaryHypergeometricSeries 𝔸 a b c n fun _ => x) = fun n =>
      ((n !⁻¹ : 𝕂) * (ascPochhammer 𝕂 n).eval a * (ascPochhammer 𝕂 n).eval b * ((ascPochhammer 𝕂 n).eval c)⁻¹) •
        x ^ n :=
  by rw [ordinaryHypergeometricSeries, ofScalars_apply_eq']

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