ordinaryHypergeometric — Mathlib

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

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