Generalized hypergeometric function

In this file we define the generalized hypergeometric function as well as the Gaussian hypergeometric function.

The hypergeometric function is a function with parameters a : Fin p → ℂ and b : Fin q → ℂ.

Note that in this file, we use the regularized version of the hypergeometric function, that is the coefficients are divides by ∏ i, Gamma (b i), giving in the case of the Gaussian hypergeometric function the series representation $$\sum_j \frac{(a)^n (b)^n}{\Gamma(c + n) n!} z^ n,$$ where (a)^n denotes the rising Pochhammer symbol.

This definition is valid for all values of c, whereas the usual hypergeometric function has a pole for c = -k and k : ℕ. To our knowledge the regularized hypergeometric function only appears in the literature only for the Gaussian case, it is implicit in the definition of the Bessel function (p = 0 and q = 1). To recover the usual hypergeometric function, simply multiply by ∏ i, Gamma (b i).

Definitions

For the general case we have

• Complex.regularizedHGFunCoeff: the coefficients
• Complex.regularizedHGFunSeries: the formal multilinear series
• Complex.regularizedHGFun: the function

For the Gaussian case (p = 2 and q = 1), we define

• Complex.regularizedGaussHGFunSeries: the formal multilinear series
• Complex.regularizedGaussHGFun: the function

Results

Convergence:

• radius_regularizedHGFunSeries_eq_top_of_finite: in the case that the series reduces to a polynomial, the radius of convergence is infinite.
• radius_regularizedHGFunSeries_eq_top: if p < q + 1, then the series has infinite convergence radius.
• radius_regularizedHGFunSeries_eq_one: if p = q + 1, then the series has convergence radius 1.
• Complex.radius_regularizedGaussHGFunSeries_eq_one: the Gaussian hypergeometric series has convergence radius 1.

noncomputable def Complex.regularizedHGFunCoeff (a b : Multiset ℂ) (n : ℕ) : ℂ

The coefficients of the regularized hypergeometric series.

Equations

• One or more equations did not get rendered due to their size.

theorem Complex.regularizedHGFunCoeff_eq_zero_iff {a b : Multiset ℂ} {n : ℕ} : regularizedHGFunCoeff a b n = 0 ↔ (∃ j ∈ a, ∃ k < n, j = -↑k) ∨ ∃ j ∈ b, ∃ (m : ℕ), j + ↑n = -↑m

theorem Complex.regularizedHGFunCoeff_eq_zero_right (a b : Multiset ℂ) (n m : ℕ) (hb : -↑n - ↑m ∈ b := by grind) : regularizedHGFunCoeff a b n = 0

theorem Complex.regularizedHGFunCoeff_eq_zero_left (a b : Multiset ℂ) (n m : ℕ) (ha : -↑m ∈ a := by grind) (hm : m < n := by grind) : regularizedHGFunCoeff a b n = 0

theorem Complex.regularizedHGFunCoeff_add_one {a b : Multiset ℂ} {n : ℕ} (hb : ∀ k ∈ b, k ≠ -↑n) : regularizedHGFunCoeff a b (n + 1) = regularizedHGFunCoeff a b n * ((Multiset.map (fun (x : ℂ) => x + ↑n) a).prod / ((Multiset.map (fun (x : ℂ) => x + ↑n) b).prod * (↑n + 1)))

Recursion formula for the coefficients of the hypergeometric series.

This is mainly used to calculate the convergence radius.

theorem Complex.regularizedHGFunCoeff_add_one_div_self {a b : Multiset ℂ} {n : ℕ} (h : regularizedHGFunCoeff a b n ≠ 0) : regularizedHGFunCoeff a b (n + 1) / regularizedHGFunCoeff a b n = (Multiset.map (fun (x : ℂ) => x + ↑n) a).prod / ((Multiset.map (fun (x : ℂ) => x + ↑n) b).prod * (↑n + 1))

Recursion formula for the coefficients of the hypergeometric series.

This is mainly used to calculate the convergence radius.

noncomputable def Complex.regularizedHGFunSeries (a b : Multiset ℂ) : FormalMultilinearSeries ℂ ℂ ℂ

The regularized hypergeometric series.

Equations

• Complex.regularizedHGFunSeries a b = FormalMultilinearSeries.ofScalars ℂ (Complex.regularizedHGFunCoeff a b)

@[simp]

theorem Complex.regularizedHGFunSeries_coeff {a b : Multiset ℂ} : (regularizedHGFunSeries a b).coeff = regularizedHGFunCoeff a b

@[simp]

theorem Complex.regularizedHGFunSeries_eq_zero {a b : Multiset ℂ} {n : ℕ} : regularizedHGFunSeries a b n = 0 ↔ regularizedHGFunCoeff a b n = 0

noncomputable def Complex.regularizedHGFun (a b : Multiset ℂ) (z : ℂ) : ℂ

The regularized hypergeometric function.

Equations

• Complex.regularizedHGFun a b z = (Complex.regularizedHGFunSeries a b).sum z

theorem Complex.radius_regularizedHGFunSeries_eq_top_of_finite {a b : Multiset ℂ} {n : ℕ} {j : ℂ} (ha : j ∈ a) (hj : j = -↑n) : (regularizedHGFunSeries a b).radius = ⊤

If there exists j and k : ℕ, such that a j = -k, then the hypergeometric series is finite and has convergence radius ∞.

theorem Complex.eventually_atTop_regularizedHGFunCoeff_ne_zero {a : Multiset ℂ} (b : Multiset ℂ) (h : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k) : ∀ᶠ (n : ℕ) in Filter.atTop, regularizedHGFunCoeff a b n ≠ 0

If for all j and k : ℕ, a j ≠ -k, then the coefficients of the hypergeometric series are eventually non-vanishing.

theorem Complex.radius_regularizedHGFunSeries_eq_top {a b : Multiset ℂ} (h : a.card ≤ b.card) : (regularizedHGFunSeries a b).radius = ⊤

If a.card ≤ b.card, then the hypergeometric series has infinite convergence radius.

theorem Complex.radius_regularizedHGFunSeries_eq_one {a b : Multiset ℂ} (h : a.card = b.card + 1) (h' : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k) : (regularizedHGFunSeries a b).radius = 1

If a.card = b.card + 1, then the hypergeometric series has convergence radius 1, unless it is a polynomial.

theorem Complex.radius_regularizedHGFunSeries_ge_one {a b : Multiset ℂ} (h : a.card = b.card + 1) : 1 ≤ (regularizedHGFunSeries a b).radius

If a.card = b.card + 1, then the hypergeometric series has convergence radius greater or equal to 1.

@[simp]

theorem Complex.regularizedHGFunSeries_zero_zero : regularizedHGFunSeries 0 0 = NormedSpace.expSeries ℂ ℂ

The regularized hypergeometric series with a = b = 0 is exponential series.

@[simp]

theorem Complex.regularizedHGFun_zero_zero : regularizedHGFun 0 0 = exp

The regularized hypergeometric function ₀F₀ is the complex exponential.

noncomputable def Complex.regularizedGaussHGFunSeries (a b c : ℂ) : FormalMultilinearSeries ℂ ℂ ℂ

The regularized Gaussian hypergeometric function.

Equations

• a.regularizedGaussHGFunSeries b c = Complex.regularizedHGFunSeries {a, b} {c}

noncomputable def Complex.regularizedGaussHGFun (a b c z : ℂ) : ℂ

The regularized Gaussian hypergeometric function.

Equations

• a.regularizedGaussHGFun b c z = (a.regularizedGaussHGFunSeries b c).sum z

theorem Complex.regularizedGaussHGFunSeries_symm (a b c : ℂ) : a.regularizedGaussHGFunSeries b c = b.regularizedGaussHGFunSeries a c

theorem Complex.regularizedGaussHGFun_symm (a b c : ℂ) : a.regularizedGaussHGFun b c = b.regularizedGaussHGFun a c

theorem Complex.coeff_regularizedGaussHGFunSeries {n : ℕ} {a b c : ℂ} : (a.regularizedGaussHGFunSeries b c).coeff n = Polynomial.eval a (ascPochhammer ℂ n) * Polynomial.eval b (ascPochhammer ℂ n) / (↑n.factorial * Gamma (c + ↑n))

theorem Complex.Gamma_inv_mul_ordinaryHypergeometricSeries_eq {a b c : ℂ} (hc : ∀ (k : ℕ), c ≠ -↑k) {n : ℕ} : (Gamma c)⁻¹ * (ordinaryHypergeometricSeries ℂ a b c).coeff n = (a.regularizedGaussHGFunSeries b c).coeff n

theorem Complex.ordinaryHypergeometric_div_Gamma_eq {a b c z : ℂ} (hc : ∀ (k : ℕ), c ≠ -↑k) : ₂F₁ a b c z / Gamma c = a.regularizedGaussHGFun b c z

@[simp]

theorem Complex.radius_regularizedGaussHGFunSeries_eq_top_of_left (b c : ℂ) (k : ℕ) : ((-↑k).regularizedGaussHGFunSeries b c).radius = ⊤

@[simp]

theorem Complex.radius_regularizedGaussHGFunSeries_eq_top_of_right (a c : ℂ) (k : ℕ) : (a.regularizedGaussHGFunSeries (-↑k) c).radius = ⊤

theorem Complex.radius_regularizedGaussHGFunSeries_eq_one {a b : ℂ} (c : ℂ) (h : ∀ (k : ℕ), a ≠ -↑k ∧ b ≠ -↑k) : (a.regularizedGaussHGFunSeries b c).radius = 1

theorem Complex.radius_regularizedGaussHGFunSeries_ge_one (a b c : ℂ) : 1 ≤ (a.regularizedGaussHGFunSeries b c).radius