1.2 Gamma and hypergeometric functions
Gamma functions give the normalization constants of the classical families. Terminating hypergeometric series give their polynomial representations.
1.2.1 Gamma and reciprocal Gamma
Write \((a)_0=1\) and \((a)_n=a(a+1)\cdots (a+n-1)\) for the rising factorial. The Gamma recurrence relates this finite product to ratios of Gamma values.
Let \(D=\mathbb C\setminus \{ 0,-1,-2,\ldots \} \). For \(z\in D\), let \(N=\lfloor \max (1-\Re z,0)\rfloor \) and define
where \(t\) ranges over the strictly positive reals and the power uses the real logarithm of \(t\). The real Gamma function is its restriction to \(\mathbb R\setminus \{ 0,-1,-2,\ldots \} \). Gamma has no assigned value at a pole.
Reference: [DLMF, 5.2.1, 5.5.1].
Lean Formalisation
def Complex.GammaPoint : TypeLean definition
/-- The complex plane with the Gamma poles removed. -/
abbrev GammaPoint := {z : ℂ // ∀ n : ℕ, z ≠ -(n : ℂ)}Every \(z\in D\) admits a natural shift into the right half-plane. For every such shift, the displayed Euler integral is integrable, \((z)_N\ne 0\), and the formula gives the same value \(\Gamma (z)\). Gamma never vanishes on \(D\), \(\Gamma (1)=1\), and
The right half-plane and all natural shifts of \(D\) lie in \(D\). For real \(x{\gt}0\), the real Euler integral is integrable and equals \(\Gamma (x){\gt}0\); the real and complex values agree on real non-poles.
Lean Formalisation
theorem Complex.GammaPoint.addNat_val (z : Complex.GammaPoint) (n : ℕ) : ↑(z.addNat n) = ↑z + ↑nLean proof
@[simp] theorem GammaPoint.addNat_val (z : GammaPoint) (n : ℕ) :
(z.addNat n).val = z.val + n := rflDefine \(G:\mathbb C\to \mathbb C\) by \(G(z)=1/\Gamma (z)\) for \(z\in D\) and \(G(-n)=0\) for \(n\ge 0\).
Reference: [DLMF, 5.2(i)].
Lean Formalisation
def Complex.reciprocalGamma (z : ℂ) : ℂLean definition
/-- The entire reciprocal Gamma function: its zeros at the poles of Gamma are
classical extension values, and inversion is used only at nonzero Gamma values. -/
def reciprocalGamma (z : ℂ) : ℂ := by
classical
exact if h : ∀ n : ℕ, z ≠ -(n : ℂ) then (GammaOn ⟨z, h⟩)⁻¹ else 0The function \(G\) is complex differentiable everywhere. Its zeros are exactly \(0,-1,-2,\ldots \), and \(G(z)\Gamma (z)=1\) for every \(z\in D\).
Lean Formalisation
theorem Complex.reciprocalGamma_mul_GammaOn (z : Complex.GammaPoint) : (↑z).reciprocalGamma * Complex.GammaOn z = 1Lean proof
/-- The reciprocal is an actual multiplicative inverse at every non-pole. -/
theorem reciprocalGamma_mul_GammaOn (z : GammaPoint) : reciprocalGamma z.val * GammaOn z = 1 := by
classical
rw [reciprocalGamma, dite_eq_left z.property]
exact inv_mul_cancel₀ (GammaOn_ne_zero z)1.2.2 The Gauss series
The coefficient definition includes terminating series. Its parameter condition ensures that every nonzero term has a nonzero denominator.
Over a field of characteristic zero, call \((a,b,c)\) admissible when \((c)_n=0\) implies \((a)_n(b)_n=0\) for every \(n\ge 0\). Its classical Gauss coefficient is zero after numerator termination; otherwise it is
In a terminating case, termination is taken before any later denominator pole; this includes coincident terminating parameters.
Reference: [DLMF, 15.2.1, 15.2.4–15.2.6].
Lean Formalisation
inductive GaussParameters.{u_2} (K : Type u_2) [Field K] [CharZero K] : Type u_2Lean definition
/-- Parameters for which no nonzero Gauss coefficient encounters a denominator pole. -/
structure GaussParameters (K : Type*) [Field K] [CharZero K] where
a : K
b : K
c : K
denominator : ∀ n : ℕ, (ascPochhammer K n).eval c = 0 →
(ascPochhammer K n).eval a * (ascPochhammer K n).eval b = 0For admissible real or complex parameters, the classical Gauss series is
Its argument domain consists exactly of the points where the partial sums in increasing natural index converge. Its value is their unique limit. The domain contains only arguments where these partial sums converge.
Reference: [DLMF, 15.2.1, 15.2.4–15.2.5].
Lean Formalisation
def GaussSeriesPoint.{u_1} {K : Type u_1} [RCLike K] (p : GaussParameters K) : Type u_1Lean definition
/-- All points where the naturally ordered classical Gauss series converges. -/
abbrev GaussSeriesPoint (p : GaussParameters K) :=
{z : K // ∃ s : K, Tendsto (fun N : ℕ ↦ ∑ n ∈ Finset.range N,
ordinaryHypergeometricCoefficientOn p n * z ^ n) atTop (𝓝 s)}The natural partial sums converge to the stated value, and every other limit of those sums agrees with it. An unconditional sum supplies this value. If either numerator is \(-k\), all coefficients after degree \(k\) vanish: every argument is in the domain and the value equals \(\sum _{n=0}^{k}u_nz^n\), allowing earlier termination. Real admissible parameters and convergent real arguments embed into the complex domains, preserving coefficients and values, including conditionally convergent and terminating series.
Lean Formalisation
theorem tendsto_ordinaryHypergeometricOn.{u_1} {K : Type u_1} [RCLike K] (p : GaussParameters K) (z : GaussSeriesPoint p) :
Filter.Tendsto (fun N => ∑ n ∈ Finset.range N, ordinaryHypergeometricCoefficientOn p n * ↑z ^ n) Filter.atTop
(nhds (ordinaryHypergeometricOn p z))Lean proof
/-- Its natural-order partial sums converge to the selected value. -/
theorem tendsto_ordinaryHypergeometricOn (p : GaussParameters K) (z : GaussSeriesPoint p) :
Tendsto (fun N : ℕ ↦ ∑ n ∈ Finset.range N,
ordinaryHypergeometricCoefficientOn p n * z.val ^ n) atTop
(𝓝 (ordinaryHypergeometricOn p z)) := z.property.choose_specFor admissible real or complex parameters, the classical Gauss series has radius at least one and converges on \(|z|{\lt}1\), where it is analytic with its defining power-series representation. Write \(F(z)={}_2F_1(a,b;c;z)\). If \(ab=0\), its first and second derivatives vanish. Otherwise \(c\ne 0\), the shifted parameters are admissible, and
In this nonconstant case, if \((a+1)(b+1)=0\), the second derivative vanishes. Otherwise the twice-shifted parameters are admissible, \(c+1\ne 0\), and
All derivatives here exist on the open disk. When \(c+j\ne 0\) for every natural \(j\), the normalized coefficient recurrence
uniquely determines the coefficients, and the genuine derivatives satisfy
Terminating cases are included. Reference: [DLMF, 15.2.1, 15.5.1, 15.10.1].
Lean Formalisation
theorem hasSum_ordinaryHypergeometricOn.{u_1} {K : Type u_1} [RCLike K] (p : GaussParameters K) (z : ↑(Metric.ball 0 1)) :
HasSum (fun n => ordinaryHypergeometricCoefficientOn p n * ↑z ^ n)
(ordinaryHypergeometricOn p (GaussSeriesPoint.ofUnitDisk p z))Lean proof
/-- The genuine classical Gauss series converges throughout the open disk. -/
theorem hasSum_ordinaryHypergeometricOn (p : GaussParameters K)
(z : Metric.ball (0 : K) 1) :
HasSum (fun n ↦ ordinaryHypergeometricCoefficientOn p n * z.val ^ n)
(ordinaryHypergeometricOn p (.ofUnitDisk p z)) := by
rcases gauss_cases p with hc | ⟨k,hk⟩
· have hs : HasSum (fun n ↦ ordinaryHypergeometricCoefficientOn p n * z.val ^ n)
(ordinaryHypergeometric p.a p.b p.c z.val) := by
simpa only [coefficient_imported_of_nonpole p hc] using
nonpole_hasSum p.a p.b p.c hc
(by simpa only [Metric.mem_ball, dist_zero_right] using z.property)
rw [ordinaryHypergeometricOn_eq_of_tendsto p (.ofUnitDisk p z) hs.tendsto_sum_nat]
exact hs
· have hs : HasSum (fun n ↦ ordinaryHypergeometricCoefficientOn p n * z.val^n)
(∑ n ∈ Finset.range (k+1), ordinaryHypergeometricCoefficientOn p n * z.val^n) :=
hasSum_sum_of_ne_finset_zero (s := Finset.range (k+1))
(f := fun n ↦ ordinaryHypergeometricCoefficientOn p n * z.val^n) (fun n hn ↦ by
rw [ordinaryHypergeometricCoefficientOn_eq_zero_of_termination p hk
(by simpa using hn), zero_mul])
rw [ordinaryHypergeometricOn_eq_of_tendsto p (.ofUnitDisk p z) hs.tendsto_sum_nat]
exact hsAdmissible parameters and coefficient recurrences
A denominator parameter outside \(\{ 0,-1,-2,\ldots \} \) always gives admissible parameters. If a numerator is \(-k\), nonvanishing denominators through degree \(k\) suffice; exchanging numerator parameters preserves admissibility. Nonzero numerator coefficients have nonzero denominators and are the displayed quotients. If \(ab=0\), all positive-degree coefficients vanish. If \(ab\ne 0\), then \(c\ne 0\), \((a+1,b+1,c+1)\) is admissible, and
Nonvanishing of \((c)_k\) implies nonvanishing of \((c)_j\) for \(j\le k\), so a single finite Pochhammer condition certifies a numerator terminating at \(k\). The pair \((-n/2,(1-n)/2)\) has one numerator equal to \(-\lfloor n/2\rfloor \); hence \((c)_{\lfloor n/2\rfloor }\ne 0\) gives admissible quadratic data. For natural \(m,k\) with \(k\le m\), \((-m)_k\ne 0\).
Lean Formalisation
theorem GaussParameters.denominator_ne_zero.{u_1} {K : Type u_1} [Field K] [CharZero K] (p : GaussParameters K) (n : ℕ)
(h : Polynomial.eval p.a (ascPochhammer K n) * Polynomial.eval p.b (ascPochhammer K n) ≠ 0) :
Polynomial.eval p.c (ascPochhammer K n) * ↑n.factorial ≠ 0Lean proof
/-- A nonzero numerator coefficient has a genuine denominator. -/
theorem GaussParameters.denominator_ne_zero (p : GaussParameters K) (n : ℕ)
(h : (ascPochhammer K n).eval p.a * (ascPochhammer K n).eval p.b ≠ 0) :
(ascPochhammer K n).eval p.c * (n.factorial : K) ≠ 0 := by
exact mul_ne_zero (fun hc ↦ h (p.denominator n hc)) (Nat.cast_ne_zero.mpr n.factorial_ne_zero)1.2.3 Regularized series
Reciprocal Gamma gives a coefficient formula that is defined even at denominator parameters where the ordinary Gauss series is unavailable.
For finite multisets \(A,B\) of complex parameters, define
where \(G\) is the reciprocal Gamma function of Definition 1.2.3.
Reference: [DLMF, 15.2.2, 16.2].
Lean Formalisation
def Complex.regularizedHGFunCoeffOn (a b : Multiset ℂ) (n : ℕ) : ℂLean definition
/-- Entire reciprocal Gamma supplies classical coefficients even at its zeros. -/
def regularizedHGFunCoeffOn (a b : Multiset ℂ) (n : ℕ) : ℂ :=
(a.map (ascPochhammer ℂ n).eval).prod *
(b.map (fun c ↦ reciprocalGamma (c + n))).prod / (n.factorial : ℂ)The regularized generalized hypergeometric value is the limit of \(\sum _{n=0}^{N-1}v_n(A;B)z^n\) as \(N\to \infty \), on exactly the domain where this limit exists. Its Gauss specialization \(\mathbf F(a,b;c;z)\) takes \(A=\{ a,b\} \) and \(B=\{ c\} \). The domain includes conditional convergence and excludes divergent series. Reference: [DLMF, 15.2.2, 16.2].
Lean Formalisation
def Complex.RegularizedHGSeriesPoint (a b : Multiset ℂ) : TypeLean definition
/-- The exact natural-order convergence domain of a regularized series. -/
abbrev RegularizedHGSeriesPoint (a b : Multiset ℂ) :=
{z : ℂ // ∃ s : ℂ, Tendsto (fun N : ℕ ↦ ∑ n ∈ Finset.range N,
regularizedHGFunCoeffOn a b n * z ^ n) atTop (𝓝 s)}If \(c\) is not a nonpositive integer and the classical ordinary Gauss series converges at \(z\), then the regularized series also converges there and \(\mathbf F(a,b;c;z)={}_2F_1(a,b;c;z)/\Gamma (c)\). The same normalization identity holds coefficient by coefficient. Reference: [DLMF, 15.2.2].
Lean Formalisation
theorem Complex.regularizedHGFunCoeffOn_eq_gauss_div_Gamma (a b : ℂ) (c : Complex.GammaPoint) (n : ℕ) :
Complex.regularizedHGFunCoeffOn {a, b} {↑c} n =
ordinaryHypergeometricCoefficientOn (GaussParameters.ofNoPole a b ↑c ⋯) n / Complex.GammaOn cLean proof
/-- Ordinary and regularized coefficients differ by the genuine Gamma factor. -/
theorem regularizedHGFunCoeffOn_eq_gauss_div_Gamma (a b : ℂ) (c : GammaPoint) (n : ℕ) :
regularizedHGFunCoeffOn {a, b} {c.val} n =
ordinaryHypergeometricCoefficientOn (.ofNoPole a b c.val c.property) n / GammaOn c := by
classical
have hcn : (ascPochhammer ℂ n).eval c.val ≠ 0 := by
intro hz
obtain ⟨k,_,hk⟩ := (ascPochhammer_eval_eq_zero_iff _ _).mp hz
exact c.property k (by simpa using congrArg Neg.neg hk.symm)
have hr : reciprocalGamma (c.val+n) = (GammaOn (c.addNat n))⁻¹ := by
change reciprocalGamma (c.addNat n).val = _
rw [reciprocalGamma, dite_eq_left (c.addNat n).property]
rw [regularizedHGFunCoeffOn_gauss, hr,
ordinaryHypergeometricCoefficientOn_eq_div _ n hcn]
dsimp only [GaussParameters.ofNoPole]
rw [← GammaOn_add_nat_div c n]
have h0 := GammaOn_ne_zero c
have hn := GammaOn_ne_zero (c.addNat n)
have hf : (n.factorial : ℂ) ≠ 0 := Nat.cast_ne_zero.mpr n.factorial_ne_zero
field_simpRegularized coefficients and convergence
For \(A=\{ a,b\} \) and \(B=\{ c\} \), \( v_n=(a)_n(b)_nG(c+n)/n!\).
Lean Formalisation
theorem Complex.regularizedHGFunCoeffOn_gauss (a b c : ℂ) (n : ℕ) :
Complex.regularizedHGFunCoeffOn {a, b} {c} n =
Polynomial.eval a (ascPochhammer ℂ n) * Polynomial.eval b (ascPochhammer ℂ n) * (c + ↑n).reciprocalGamma /
↑n.factorialLean proof
/-- The regularized Gauss coefficients in their classical form. -/
theorem regularizedHGFunCoeffOn_gauss (a b c : ℂ) (n : ℕ) :
regularizedHGFunCoeffOn {a, b} {c} n =
(ascPochhammer ℂ n).eval a * (ascPochhammer ℂ n).eval b *
reciprocalGamma (c + n) / (n.factorial : ℂ) := by
simp [regularizedHGFunCoeffOn]The natural partial sums converge to the regularized value, uniquely. Every unconditional sum is also this natural-order sum and supplies a point of the domain.
Lean Formalisation
theorem Complex.tendsto_regularizedHGFunOn (a b : Multiset ℂ) (z : Complex.RegularizedHGSeriesPoint a b) :
Filter.Tendsto (fun N => ∑ n ∈ Finset.range N, Complex.regularizedHGFunCoeffOn a b n * ↑z ^ n) Filter.atTop
(nhds (Complex.regularizedHGFunOn a b z))Lean proof
/-- Natural partial sums converge to the classical regularized value. -/
theorem tendsto_regularizedHGFunOn (a b : Multiset ℂ)
(z : RegularizedHGSeriesPoint a b) :
Tendsto (fun N : ℕ ↦ ∑ n ∈ Finset.range N,
regularizedHGFunCoeffOn a b n * z.val ^ n) atTop (𝓝 (regularizedHGFunOn a b z)) :=
z.property.choose_spec