Ordinary hypergeometric function in a Banach algebra

In this file, we define ordinaryHypergeometric, the ordinary or Gaussian hypergeometric function in a topological algebra 𝔸 over a field 𝕂 given by: $$ _2\mathrm{F}_1(a\ b\ c : \mathbb{K}, x : \mathbb{A}) = \sum_{n=0}^{\infty}\frac{(a)_n(b)_n}{(c)_n} \frac{x^n}{n!} \,, $$ with $(a)_n$ is the ascending Pochhammer symbol (see ascPochhammer).

This file contains the basic definitions over a general field 𝕂 and notation for ₂F₁, as well as showing that terms of the series are zero if any of the (a b c : 𝕂) are sufficiently large non-positive integers, rendering the series finite. In this file "sufficiently large" means that -n < a for the n-th term, and similarly for b and c.

• ordinaryHypergeometricSeries is the FormalMultilinearSeries given above for some (a b c : 𝕂)
• ordinaryHypergeometric is the sum of the series for some (x : 𝔸)
• ordinaryHypergeometricSeries_eq_zero_of_nonpos_int shows that the n-th term of the series is zero if any of the parameters are sufficiently large non-positive integers

[RCLike 𝕂]

If we have [RCLike 𝕂], then we show that the latter result is an iff, and hence prove that the radius of convergence of the series is unity if the series is infinite, or ⊤ otherwise.

• ordinaryHypergeometricSeries_eq_zero_iff is iff variant of ordinaryHypergeometricSeries_eq_zero_of_nonpos_int
• ordinaryHypergeometricSeries_radius_eq_one proves that the radius of convergence of the ordinaryHypergeometricSeries is unity under non-trivial parameters

Notation

₂F₁ is notation for ordinaryHypergeometric.

References

See https://en.wikipedia.org/wiki/Hypergeometric_function.

Tags

hypergeometric, gaussian, ordinary

@[reducible, inline]

noncomputable abbrev ordinaryHypergeometricCoefficient {𝕂 : Type u_1} [Field 𝕂] (a : 𝕂) (b : 𝕂) (c : 𝕂) (n : ℕ) : 𝕂

The coefficients in the ordinary hypergeometric sum.

Equations

• ordinaryHypergeometricCoefficient a b c n = (↑n.factorial)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) * (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹

noncomputable def ordinaryHypergeometricSeries {𝕂 : Type u_1} (𝔸 : Type u_2) [Field 𝕂] [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] (a : 𝕂) (b : 𝕂) (c : 𝕂) : FormalMultilinearSeries 𝕂 𝔸 𝔸

ordinaryHypergeometricSeries 𝔸 (a b c : 𝕂) is a FormalMultilinearSeries. Its sum is the ordinaryHypergeometric map.

Equations

• ordinaryHypergeometricSeries 𝔸 a b c = FormalMultilinearSeries.ofScalars 𝔸 (ordinaryHypergeometricCoefficient a b c)

noncomputable def ordinaryHypergeometric {𝕂 : Type u_1} {𝔸 : Type u_2} [Field 𝕂] [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] (a : 𝕂) (b : 𝕂) (c : 𝕂) (x : 𝔸) : 𝔸

ordinaryHypergeometric (a b c : 𝕂) : 𝔸 → 𝔸 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.

Equations

• ₂F₁ a b c x = (ordinaryHypergeometricSeries 𝔸 a b c).sum x

def term₂F₁ : Lean.ParserDescr

ordinaryHypergeometric (a b c : 𝕂) : 𝔸 → 𝔸 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.

Equations

• term₂F₁ = Lean.ParserDescr.node `term₂F₁ 1024 (Lean.ParserDescr.symbol "₂F₁")

theorem ordinaryHypergeometricSeries_apply_eq {𝕂 : Type u_1} {𝔸 : Type u_2} [Field 𝕂] [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] (a : 𝕂) (b : 𝕂) (c : 𝕂) (x : 𝔸) (n : ℕ) : ((ordinaryHypergeometricSeries 𝔸 a b c n) fun (x_1 : Fin n) => x) = ((↑n.factorial)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) * (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹) • x ^ n

theorem ordinaryHypergeometricSeries_apply_eq' {𝕂 : Type u_1} {𝔸 : Type u_2} [Field 𝕂] [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] (a : 𝕂) (b : 𝕂) (c : 𝕂) (x : 𝔸) : (fun (n : ℕ) => (ordinaryHypergeometricSeries 𝔸 a b c n) fun (x_1 : Fin n) => x) = fun (n : ℕ) => ((↑n.factorial)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) * (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹) • x ^ n

This naming follows the convention of NormedSpace.expSeries_apply_eq'.

theorem ordinaryHypergeometric_sum_eq {𝕂 : Type u_1} {𝔸 : Type u_2} [Field 𝕂] [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] (a : 𝕂) (b : 𝕂) (c : 𝕂) (x : 𝔸) : (ordinaryHypergeometricSeries 𝔸 a b c).sum x = ∑' (n : ℕ), ((↑n.factorial)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) * (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹) • x ^ n

theorem ordinaryHypergeometric_eq_tsum {𝕂 : Type u_1} {𝔸 : Type u_2} [Field 𝕂] [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] (a : 𝕂) (b : 𝕂) (c : 𝕂) : ₂F₁ a b c = fun (x : 𝔸) => ∑' (n : ℕ), ((↑n.factorial)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) * (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹) • x ^ n

theorem ordinaryHypergeometricSeries_apply_zero {𝕂 : Type u_1} {𝔸 : Type u_2} [Field 𝕂] [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] (a : 𝕂) (b : 𝕂) (c : 𝕂) (n : ℕ) : ((ordinaryHypergeometricSeries 𝔸 a b c n) fun (x : Fin n) => 0) = Pi.single 0 1 n

@[simp]

theorem ordinaryHypergeometric_zero {𝕂 : Type u_1} {𝔸 : Type u_2} [Field 𝕂] [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] (a : 𝕂) (b : 𝕂) (c : 𝕂) : ₂F₁ a b c 0 = 1

theorem ordinaryHypergeometricSeries_symm {𝕂 : Type u_1} {𝔸 : Type u_2} [Field 𝕂] [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] (a : 𝕂) (b : 𝕂) (c : 𝕂) : ordinaryHypergeometricSeries 𝔸 a b c = ordinaryHypergeometricSeries 𝔸 b a c

theorem ordinaryHypergeometricSeries_eq_zero_of_neg_nat {𝕂 : Type u_1} {𝔸 : Type u_2} [Field 𝕂] [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] (a : 𝕂) (b : 𝕂) (c : 𝕂) {n : ℕ} {k : ℕ} (habc : ↑k = -a ∨ ↑k = -b ∨ ↑k = -c) (hk : k < n) : ordinaryHypergeometricSeries 𝔸 a b c n = 0

If any parameter to the series is a sufficiently large nonpositive integer, then the series term is zero.

theorem ordinaryHypergeometric_radius_top_of_neg_nat₁ {𝕂 : Type u_1} (𝔸 : Type u_2) [RCLike 𝕂] [NormedDivisionRing 𝔸] [NormedAlgebra 𝕂 𝔸] (b : 𝕂) (c : 𝕂) {k : ℕ} : (ordinaryHypergeometricSeries 𝔸 (-↑k) b c).radius = ⊤

theorem ordinaryHypergeometric_radius_top_of_neg_nat₂ {𝕂 : Type u_1} (𝔸 : Type u_2) [RCLike 𝕂] [NormedDivisionRing 𝔸] [NormedAlgebra 𝕂 𝔸] (a : 𝕂) (c : 𝕂) {k : ℕ} : (ordinaryHypergeometricSeries 𝔸 a (-↑k) c).radius = ⊤

theorem ordinaryHypergeometric_radius_top_of_neg_nat₃ {𝕂 : Type u_1} (𝔸 : Type u_2) [RCLike 𝕂] [NormedDivisionRing 𝔸] [NormedAlgebra 𝕂 𝔸] (a : 𝕂) (b : 𝕂) {k : ℕ} : (ordinaryHypergeometricSeries 𝔸 a b (-↑k)).radius = ⊤

theorem ordinaryHypergeometricSeries_eq_zero_iff {𝕂 : Type u_1} (𝔸 : Type u_2) [RCLike 𝕂] [NormedDivisionRing 𝔸] [NormedAlgebra 𝕂 𝔸] (a : 𝕂) (b : 𝕂) (c : 𝕂) (n : ℕ) : ordinaryHypergeometricSeries 𝔸 a b c n = 0 ↔ ∃ k < n, ↑k = -a ∨ ↑k = -b ∨ ↑k = -c

An iff variation on ordinaryHypergeometricSeries_eq_zero_of_nonpos_int for [RCLike 𝕂].

theorem ordinaryHypergeometricSeries_norm_div_succ_norm {𝕂 : Type u_1} [RCLike 𝕂] (a : 𝕂) (b : 𝕂) (c : 𝕂) (n : ℕ) (habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c) : ‖ordinaryHypergeometricCoefficient a b c n‖ / ‖ordinaryHypergeometricCoefficient a b c n.succ‖ = ‖a + ↑n‖⁻¹ * ‖b + ↑n‖⁻¹ * ‖c + ↑n‖ * ‖1 + ↑n‖

theorem ordinaryHypergeometricSeries_radius_eq_one {𝕂 : Type u_1} (𝔸 : Type u_2) [RCLike 𝕂] [NormedDivisionRing 𝔸] [NormedAlgebra 𝕂 𝔸] (a : 𝕂) (b : 𝕂) (c : 𝕂) (habc : ∀ (kn : ℕ), ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c) : (ordinaryHypergeometricSeries 𝔸 a b c).radius = 1

The radius of convergence of ordinaryHypergeometricSeries is unity if none of the parameters are non-positive integers.