English
Equality of the hypergeometric series with its sum map: the sum of ordinaryHypergeometricSeries equals the ordinaryHypergeometric map.
Русский
Сумма гипергеометрической серии равна соответствующему отображению ₂F₁.
LaTeX
$$$\\big( ordinaryHypergeometricSeries(\\mathbb{A}, a,b,c) \\big).sum x = \\text{ordinaryHypergeometric}(a,b,c)(x)$$$
Lean4
/-- `ordinaryHypergeometric (a b c : 𝕂) : 𝔸 → 𝔸`, denoted `₂F₁`, is the ordinary hypergeometric map,
defined as the sum of the `FormalMultilinearSeries` `ordinaryHypergeometricSeries 𝔸 a b c`.
Note that this takes the junk value `0` outside the radius of convergence.
-/
noncomputable def ordinaryHypergeometric (x : 𝔸) : 𝔸 :=
(ordinaryHypergeometricSeries 𝔸 a b c).sum x