ordinaryHypergeometricSeries — Mathlib

English

The ordinary hypergeometric series is the formal multilinear series whose nth coefficient is the ordinaryHypergeometricCoefficient and sum encodes the hypergeometric function ₂F₁.

Русский

Обыкновенный гипергеометрический ряд – это формальная многочлическая (мультилинейная) серия, где n-й коэффициент – ordinaryHypergeometricCoefficient и сумма даёт функцию ₂F₁.

LaTeX

$$$\\text{ordinaryHypergeometricSeries}(a,b,c) : \\mathcal{FS}_{\\mathbb{K}}(\\mathbb{A})$ with nth coefficient given by ordinaryHypergeometricCoefficient$$

Lean4

/-- `ordinaryHypergeometricSeries 𝔸 (a b c : 𝕂)` is a `FormalMultilinearSeries`.
Its sum is the `ordinaryHypergeometric` map. -/
noncomputable def ordinaryHypergeometricSeries (a b c : 𝕂) : FormalMultilinearSeries 𝕂 𝔸 𝔸 :=
  ofScalars 𝔸 (ordinaryHypergeometricCoefficient a b c)

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