ordinaryHypergeometric_sum_eq — Mathlib

English

Congruence property: the ordinary hypergeometric series is invariant under certain parameter relabellings, i.e., a ↔ b symmetry.

Русский

Свойство неизменности гипергеометрического ряда при симметрии параметров a и b.

LaTeX

$$$\\ordinaryHypergeometricSeries(a,b,c) = \\ordinaryHypergeometricSeries(b,a,c)$$$

Lean4

theorem ordinaryHypergeometric_sum_eq (x : 𝔸) :
    (ordinaryHypergeometricSeries 𝔸 a b c).sum x =
      ∑' n : ℕ,
        ((n !⁻¹ : 𝕂) * (ascPochhammer 𝕂 n).eval a * (ascPochhammer 𝕂 n).eval b * ((ascPochhammer 𝕂 n).eval c)⁻¹) •
          x ^ n :=
  tsum_congr fun n => ordinaryHypergeometricSeries_apply_eq a b c x n

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