Clausen's formula and the hypergeometric differential equations

This file covers chapter 6 of Milla's proof of the Chudnovsky formula (arXiv:1809.00533v6, 110_Clausen.tex), together with the representation theorem darst from chapter 9 (140_MainTheorem.tex) and the Pochhammer/factorial identity used in its proof.

Main definitions

• generalizedHypergeometric (notation ₃F₂): the generalized hypergeometric function ₃F₂(α, β, γ; δ, ε; z) = ∑ (α)ₙ(β)ₙ(γ)ₙ / ((δ)ₙ(ε)ₙ) · zⁿ/n! (paper Def. defihyp), defined in a topological algebra by mirroring Mathlib's ordinaryHypergeometric (₂F₁);
• Chudnovsky.hyp2F1: the specific instance ₂F₁(1/12, 5/12; 1; z);
• Chudnovsky.hyp3F2: the specific instance ₃F₂(1/6, 5/6, 1/2; 1, 1; z).

Main statements

• generalizedHypergeometric_summable : absolute convergence for ‖z‖ < 1 (paper Thm. satzkonv; the ₂F₁ analogue is Mathlib's ordinaryHypergeometricSeries_radius_eq_one);
• ordinaryHypergeometric_ode : the second-order hypergeometric ODE for ₂F₁ (paper Thm. dgl2f1);
• generalizedHypergeometric_ode : the third-order ODE for ₃F₂ (paper Thm. dgl3f2);
• clausen_formula : Clausen's formula (₂F₁(a, b; a+b+1/2; z))² = ₃F₂(2a, 2b, a+b; 2a+2b, a+b+1/2; z) (paper Thm. satzclausen);
• Chudnovsky.hyp2F1_sq_eq_hyp3F2 : its specialization at a = 1/12, b = 5/12;
• Chudnovsky.ascPochhammer_prod_eq_factorial : the Pochhammer/factorial identity (1/6)ₙ(1/2)ₙ(5/6)ₙ = (6n)! / ((3n)!·12^(3n)) over ℚ (paper, proof of darst);
• Chudnovsky.hyp2F1_sq_eq_tsum : the representation (₂F₁(1/12, 5/12; 1; z))² = ∑ (6n)!/((3n)!(n!)³) · zⁿ/12^(3n) (paper Thm. darst).

The generalized hypergeometric function ₃F₂ (paper Def. defihyp)

The definitions mirror Mathlib/Analysis/SpecialFunctions/OrdinaryHypergeometric.lean.

@[reducible, inline]

noncomputable abbrev generalizedHypergeometricCoefficient {𝕂 : Type u_1} [Field 𝕂] (α β γ δ ε : 𝕂) (n : ℕ) : 𝕂

The coefficients in the generalized hypergeometric sum: (α)ₙ(β)ₙ(γ)ₙ / ((δ)ₙ(ε)ₙ n!), mirroring ordinaryHypergeometricCoefficient.

Equations

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

noncomputable def generalizedHypergeometricSeries {𝕂 : Type u_1} (𝔸 : Type u_2) [Field 𝕂] [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [IsTopologicalRing 𝔸] (α β γ δ ε : 𝕂) : FormalMultilinearSeries 𝕂 𝔸 𝔸

generalizedHypergeometricSeries 𝔸 (α β γ δ ε : 𝕂) is a FormalMultilinearSeries. Its sum is the generalizedHypergeometric map.

Equations

• generalizedHypergeometricSeries 𝔸 α β γ δ ε = FormalMultilinearSeries.ofScalars 𝔸 (generalizedHypergeometricCoefficient α β γ δ ε)

noncomputable def generalizedHypergeometric {𝕂 : Type u_1} {𝔸 : Type u_2} [Field 𝕂] [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [IsTopologicalRing 𝔸] (α β γ δ ε : 𝕂) (x : 𝔸) : 𝔸

generalizedHypergeometric (α β γ δ ε : 𝕂) : 𝔸 → 𝔸, denoted ₃F₂, is the generalized hypergeometric map, defined as the sum of the FormalMultilinearSeries generalizedHypergeometricSeries 𝔸 α β γ δ ε.

Note that this takes the junk value 0 outside the radius of convergence.

Equations

• ₃F₂ α β γ δ ε x = (generalizedHypergeometricSeries 𝔸 α β γ δ ε).sum x

def term₃F₂ : Lean.ParserDescr

generalizedHypergeometric (α β γ δ ε : 𝕂) : 𝔸 → 𝔸, denoted ₃F₂, is the generalized hypergeometric map, defined as the sum of the FormalMultilinearSeries generalizedHypergeometricSeries 𝔸 α β γ δ ε.

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 generalizedHypergeometricSeries_apply_eq {𝕂 : Type u_1} {𝔸 : Type u_2} [Field 𝕂] [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [IsTopologicalRing 𝔸] (α β γ δ ε : 𝕂) (x : 𝔸) (n : ℕ) : ((generalizedHypergeometricSeries 𝔸 α β γ δ ε n) fun (x_1 : Fin n) => x) = generalizedHypergeometricCoefficient α β γ δ ε n • x ^ n

theorem generalizedHypergeometric_sum_eq {𝕂 : Type u_1} {𝔸 : Type u_2} [Field 𝕂] [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [IsTopologicalRing 𝔸] (α β γ δ ε : 𝕂) (x : 𝔸) : (generalizedHypergeometricSeries 𝔸 α β γ δ ε).sum x = ∑' (n : ℕ), generalizedHypergeometricCoefficient α β γ δ ε n • x ^ n

theorem generalizedHypergeometric_eq_tsum {𝕂 : Type u_1} {𝔸 : Type u_2} [Field 𝕂] [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [IsTopologicalRing 𝔸] (α β γ δ ε : 𝕂) : ₃F₂ α β γ δ ε = fun (x : 𝔸) => ∑' (n : ℕ), generalizedHypergeometricCoefficient α β γ δ ε n • x ^ n

theorem generalizedHypergeometricSeries_apply_zero {𝕂 : Type u_1} {𝔸 : Type u_2} [Field 𝕂] [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [IsTopologicalRing 𝔸] (α β γ δ ε : 𝕂) (n : ℕ) : ((generalizedHypergeometricSeries 𝔸 α β γ δ ε n) fun (x : Fin n) => 0) = Pi.single 0 1 n

@[simp]

theorem generalizedHypergeometric_zero {𝕂 : Type u_1} {𝔸 : Type u_2} [Field 𝕂] [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [IsTopologicalRing 𝔸] (α β γ δ ε : 𝕂) : ₃F₂ α β γ δ ε 0 = 1

Convergence (paper Thm. satzkonv)

theorem generalizedHypergeometricSeries_radius_eq_one {𝕂 : Type u_1} (𝔸 : Type u_2) [RCLike 𝕂] [NormedDivisionRing 𝔸] [NormedAlgebra 𝕂 𝔸] (α β γ δ ε : 𝕂) (h : ∀ (kn : ℕ), ↑kn ≠ -α ∧ ↑kn ≠ -β ∧ ↑kn ≠ -γ ∧ ↑kn ≠ -δ ∧ ↑kn ≠ -ε) : (generalizedHypergeometricSeries 𝔸 α β γ δ ε).radius = 1

The radius of convergence of generalizedHypergeometricSeries is unity if none of the parameters are non-positive integers, mirroring ordinaryHypergeometricSeries_radius_eq_one.

theorem generalizedHypergeometric_summable (α β γ δ ε : ℂ) {z : ℂ} (hz : ‖z‖ < 1) : Summable fun (n : ℕ) => generalizedHypergeometricCoefficient α β γ δ ε n * z ^ n

Paper Thm. satzkonv: the generalized hypergeometric series converges absolutely for ‖z‖ < 1 (ratio test). The ₂F₁ analogue is Mathlib's ordinaryHypergeometricSeries_radius_eq_one.

Term-by-term differentiation of scalar power series on the open unit disc

General infrastructure used to prove the hypergeometric ODEs. For a coefficient sequence c : ℕ → ℂ whose power series is absolutely convergent on the open unit disc, the sum z ↦ ∑' n, cₙ zⁿ is differentiable there, with derivative ∑' n, (n+1) c₍ₙ₊₁₎ zⁿ.

The hypergeometric differential equations (paper Thms. dgl2f1, dgl3f2)

theorem ordinaryHypergeometric_ode (a b c : ℂ) (hc : ∀ (k : ℕ), ↑k ≠ -c) {z : ℂ} (hz : ‖z‖ < 1) : z * (z - 1) * deriv (deriv fun (w : ℂ) => ₂F₁ a b c w) z + ((a + b + 1) * z - c) * deriv (fun (w : ℂ) => ₂F₁ a b c w) z + a * b * ₂F₁ a b c z = 0

Paper Thm. dgl2f1: on the unit disc, f = ₂F₁(a, b; c; ·) satisfies the hypergeometric differential equation z(z-1)f'' + [(a+b+1)z - c]f' + ab·f = 0.

The hypothesis hc (c is not a non-positive integer) is implicit in the paper: without it Mathlib's junk-value conventions make the series terms vanish for large n and the ODE fails.

theorem generalizedHypergeometric_ode (α β γ δ ε : ℂ) (hδ : ∀ (k : ℕ), ↑k ≠ -δ) (hε : ∀ (k : ℕ), ↑k ≠ -ε) {z : ℂ} (hz : ‖z‖ < 1) : (z ^ 3 - z ^ 2) * deriv (deriv (deriv fun (w : ℂ) => ₃F₂ α β γ δ ε w)) z + ((α + β + γ + 3) * z ^ 2 - (δ + ε + 1) * z) * deriv (deriv fun (w : ℂ) => ₃F₂ α β γ δ ε w) z + ((α * β + α * γ + β * γ + α + β + γ + 1) * z - δ * ε) * deriv (fun (w : ℂ) => ₃F₂ α β γ δ ε w) z + α * β * γ * ₃F₂ α β γ δ ε z = 0

Paper Thm. dgl3f2: on the unit disc, g = ₃F₂(α, β, γ; δ, ε; ·) satisfies the third-order differential equation (z³-z²)g''' + [(α+β+γ+3)z² - (δ+ε+1)z]g'' + [(1+α+β+γ+αβ+αγ+βγ)z - δε]g' + αβγ·g = 0.

The hypotheses hδ, hε are implicit in the paper (cf. ordinaryHypergeometric_ode).

Clausen's formula (paper Thm. satzclausen)

theorem clausen_formula (a b : ℂ) (h₁ : ∀ (k : ℕ), ↑k ≠ -(a + b + 1 / 2)) (h₂ : ∀ (k : ℕ), ↑k ≠ -(2 * a + 2 * b)) {z : ℂ} (hz : ‖z‖ < 1) : ₂F₁ a b (a + b + 1 / 2) z ^ 2 = ₃F₂ (2 * a) (2 * b) (a + b) (2 * a + 2 * b) (a + b + 1 / 2) z

Clausen's formula (paper Thm. satzclausen, Clausen 1828): for ‖z‖ < 1, (₂F₁(a, b; a+b+1/2; z))² = ₃F₂(2a, 2b, a+b; 2a+2b, a+b+1/2; z).

The non-degeneracy hypotheses h₁, h₂ on the lower parameters are implicit in the paper (they hold in the only instance used, a = 1/12, b = 5/12).

theorem ascPochhammer_eval_ratCast (n : ℕ) (q : ℚ) : ↑(Polynomial.eval q (ascPochhammer ℚ n)) = Polynomial.eval (↑q) (ascPochhammer ℂ n)

Evaluating an ascending Pochhammer polynomial at a rational point commutes with the ℚ → ℂ coercion.

theorem ordinaryHypergeometricCoefficient_ratCast (a b c : ℚ) (n : ℕ) : ↑(ordinaryHypergeometricCoefficient a b c n) = ordinaryHypergeometricCoefficient (↑a) (↑b) (↑c) n

The ₂F₁ coefficient commutes with the ℚ → ℂ coercion.

theorem generalizedHypergeometricCoefficient_ratCast (α β γ δ ε : ℚ) (n : ℕ) : ↑(generalizedHypergeometricCoefficient α β γ δ ε n) = generalizedHypergeometricCoefficient (↑α) (↑β) (↑γ) (↑δ) (↑ε) n

The ₃F₂ coefficient commutes with the ℚ → ℂ coercion.

theorem ordinaryHypergeometric_norm_summable (a b c : ℂ) (h : ∀ (kn : ℕ), ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c) {z : ℂ} (hz : ‖z‖ < 1) : Summable fun (n : ℕ) => ‖ordinaryHypergeometricCoefficient a b c n * z ^ n‖

If none of a, b, c is a non-positive integer, the ₂F₁ series is absolutely convergent for ‖z‖ < 1 (norm-summable coefficients). Mirrors generalizedHypergeometric_summable.

The specific instances used in the paper

noncomputable def Chudnovsky.hyp2F1 (z : ℂ) : ℂ

The hypergeometric function ₂F₁(1/12, 5/12; 1; z) (paper Thms. darst, omegastrich).

Equations

• Chudnovsky.hyp2F1 z = ₂F₁ (1 / 12) (5 / 12) 1 z

noncomputable def Chudnovsky.hyp3F2 (z : ℂ) : ℂ

The generalized hypergeometric function ₃F₂(1/6, 5/6, 1/2; 1, 1; z), the right-hand side of Clausen's formula at a = 1/12, b = 5/12 (paper Thm. satzclausen).

Equations

• Chudnovsky.hyp3F2 z = ₃F₂ (1 / 6) (5 / 6) (1 / 2) 1 1 z

Proof of the Clausen coefficient identity by a WZ/creative-telescoping recurrence

Writing cₖ = (1/12)ₖ(5/12)ₖ/(k!)² and dₙ = (1/6)ₙ(5/6)ₙ(1/2)ₙ/(n!)³, we show eₙ := ∑_{k=0}^n cₖ c_{n-k} equals dₙ by proving both satisfy the same first-order recurrence (n+1)³ · x_{n+1} = (n+1/6)(n+1/2)(n+5/6) · xₙ.

The recurrence for eₙ is a creative-telescoping identity: with the WZ certificate gₙ(k) := k²(2k-3n-3) cₖ c_{n+1-k} one has, for k ≤ n, (n+1)³ cₖ c_{n+1-k} - (n+1/6)(n+1/2)(n+5/6) cₖ c_{n-k} = gₙ(k+1) - gₙ(k), and summing over k = 0,…,n telescopes (both boundary terms cancel automatically).

theorem Chudnovsky.clausen_coeff_identity (n : ℕ) : ∑ k ∈ Finset.range (n + 1), ordinaryHypergeometricCoefficient (1 / 12) (5 / 12) 1 k * ordinaryHypergeometricCoefficient (1 / 12) (5 / 12) 1 (n - k) = generalizedHypergeometricCoefficient (1 / 6) (5 / 6) (1 / 2) 1 1 n

The finite coefficient identity underlying Clausen's formula at a = 1/12, b = 5/12, stated over ℚ. The left-hand side is the n-th Cauchy-product coefficient of (₂F₁(1/12, 5/12; 1; ·))² and the right-hand side is the n-th coefficient of ₃F₂(1/6, 5/6, 1/2; 1, 1; ·). Equivalently, writing cₖ = (1/12)ₖ(5/12)ₖ/(k!)² and dₙ = (6n)!/((3n)!(n!)³·1728ⁿ), this is ∑_{k=0}^n cₖ c_{n-k} = dₙ.

theorem Chudnovsky.hyp2F1_sq_eq_hyp3F2 {z : ℂ} (hz : ‖z‖ < 1) : hyp2F1 z ^ 2 = hyp3F2 z

Clausen's formula specialized to a = 1/12, b = 5/12 (paper Thm. satzclausen): (₂F₁(1/12, 5/12; 1; z))² = ₃F₂(1/6, 5/6, 1/2; 1, 1; z) for ‖z‖ < 1.

The analytic reduction (Cauchy product of the square, coefficient comparison) is carried out here; the remaining arithmetic core is clausen_coeff_identity.

theorem Chudnovsky.ascPochhammer_prod_eq_factorial (n : ℕ) : Polynomial.eval (1 / 6) (ascPochhammer ℚ n) * Polynomial.eval (1 / 2) (ascPochhammer ℚ n) * Polynomial.eval (5 / 6) (ascPochhammer ℚ n) = ↑(6 * n).factorial / (↑(3 * n).factorial * 12 ^ (3 * n))

The Pochhammer/factorial identity from the proof of paper Thm. darst: (1/6)ₙ · (1/2)ₙ · (5/6)ₙ = (6n)! / ((3n)! · 12^(3n)), stated over ℚ.

theorem Chudnovsky.hyp2F1_sq_eq_tsum {z : ℂ} (hz : ‖z‖ < 1) : hyp2F1 z ^ 2 = ∑' (n : ℕ), ↑(6 * n).factorial / (↑(3 * n).factorial * ↑n.factorial ^ 3) * (z ^ n / 12 ^ (3 * n))

Paper Thm. darst (chapter 9, 140_MainTheorem.tex): for ‖z‖ < 1, (₂F₁(1/12, 5/12; 1; z))² = ∑ (6n)!/((3n)!(n!)³) · zⁿ/12^(3n). Note 12^(3n) = 1728^n.