Kummer's solution of the Picard–Fuchs equation

This file covers chapter 8 of Milla's proof of the Chudnovsky formula (arXiv:1809.00533v6, 130_Kummer.tex).

Main definitions

• Chudnovsky.kummerB : Kummer's solution b(J) = J^(-1/4) · (1-J)^(1/4) · ₂F₁(1/12, 5/12; 1; 1/J) (paper Thm. satzbj), realized with principal-branch cpow. (The paper allows an arbitrary fixed branch of the fourth roots; since the Picard–Fuchs equation is homogeneous the choice is immaterial there.)

Main statements (all proved)

• Chudnovsky.kummerB_satisfiesPicardFuchs : b(J) solves the Picard–Fuchs equation (paper Thm. satzbj). The paper states this for all |J| > 1; with the principal branch we must additionally stay off the branch cuts, i.e. off the real axis (for J real with |J| > 1 either J or 1 - J is a negative real).
• Chudnovsky.norm_inv_J_lt_one : 1/J(τ) lies in the unit disc on Region (from Estimates.lean's one_lt_norm_J), so that the hypergeometric series converges.
• Chudnovsky.E₄_eq_hyp2F1_pow_four : the chapter's output omegastrich, in the branch-free fourth-power form recommended by PLAN A7: E₄(τ) = (₂F₁(1/12, 5/12; 1; 1/J(τ)))⁴ for τ ∈ Region, proved by the Wronskian comparison argument described in the section OmegaStrich below (using Ramanujan's derivative identities from Ramanujan.lean in place of the paper's period integrals).

Faithfulness note on omegastrich

The paper's Thm. omegastrich reads Δ(τ)^(1/12) = (2π / 12^(1/4)) · J(τ)^(-1/12) · ₂F₁(1/12, 5/12; 1; 1/J(τ)), with all roots determined only up to roots of unity until the Main Theorem's connectedness argument (paper Remark bemwurzel); here Δ is the lattice discriminant g₂³ - 27g₃² = (2π)¹² · Δ_Mathlib. Raising to the 12th power and using 1728·J = E₄³/Δ_Mathlib (Chudnovsky.mul_J_eq) gives the branch-free equivalent E₄³ = F¹²; the classical (and correct on Region) branch refinement is E₄ = F⁴, which is what chapter 9 consumes after the PLAN A7 reformulation. TODO: if the final assembly of MainTheorem.lean turns out to need the literal Δ^(1/12) statement (it uses ωtilde₁ = Δ^(1/12) only through F and dF/dJ), add it here with an explicit principal-branch bookkeeping.

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

Kummer's solution b(J) = J^(-1/4) · (1-J)^(1/4) · ₂F₁(1/12, 5/12; 1; 1/J) of the Picard–Fuchs equation (paper Thm. satzbj), taken with principal-branch complex powers.

Equations

• Chudnovsky.kummerB z = z ^ (-(1 / 4)) * (1 - z) ^ (1 / 4) * Chudnovsky.hyp2F1 z⁻¹

theorem Chudnovsky.kummerB_satisfiesPicardFuchs : SatisfiesPicardFuchs kummerB {z : ℂ | 1 < ‖z‖ ∧ z.im ≠ 0}

Paper Thm. satzbj: Kummer's function b(J) solves the Picard–Fuchs differential equation on |J| > 1.

TODO: the paper's statement holds for |J| > 1 with any fixed branch of the fourth roots; with the principal branch (Complex.cpow) we restrict to the complement of the real axis, where both z ↦ z^(-1/4) and z ↦ (1-z)^(1/4) are holomorphic (J real with |J| > 1 makes J or 1 - J a negative real, i.e. lie on the principal branch cut).

theorem Chudnovsky.norm_inv_J_lt_one {τ : UpperHalfPlane} (hτ : τ ∈ Region) : ‖(J τ)⁻¹‖ < 1

On Region, the argument 1/J(τ) of the hypergeometric function lies in the open unit disc (via Estimates.lean's one_lt_norm_J).

The branch-free omegastrich: E₄ = ₂F₁(1/12, 5/12; 1; 1/J)⁴ on Region

The proof follows the "differentiate and compare" strategy of PLAN A7, in a Wronskian form that needs no quantitative estimates near i∞:

1. Near i∞, the hypergeometric pair (X, Y) = (F(1/J), F′(1/J)) (with F = ₂F₁(1/12, 5/12; 1; ·)) and the modular pair (Xtilde, Ytilde) = (E₄^{1/4}, E₄^{1/4}·E₄³·(E₂E₄-E₆)/(12·(E₄³-E₆²)·E₆)) both solve the same linear 2×2 system D Z = M(τ)·Z: the first by the hypergeometric ODE and the chain rule with D (1/J) = (1/J)·E₆/E₄ (from Ramanujan's identities), the second again by Ramanujan's identities. Here M₁₂ = (1/J)E₆/E₄, M₂₁ = (5/144)E₄²/E₆, M₂₂ = ((3/2)(1/J) - 1)·E₄²/E₆, and the principal branch E₄^{1/4} is harmless since E₄ ≈ 1 near i∞.
2. The Wronskian w = XYtilde - YXtilde solves the scalar ODE D w = M₂₂·w where M₂₂ → -1 at i∞. Along each vertical line t ↦ x₀ + it the function t ↦ ‖w‖²·e^{-2πt} is monotone nondecreasing (as soon as Re M₂₂ ≤ -1/2), while w → 0 at i∞ (both pairs converge to (1, 5/144)); hence w ≡ 0.
3. w ≡ 0 forces (Xtilde/X)′ = 0, so Xtilde/X is constant = 1 (its limit at i∞) on {Im τ > A}, whence E₄ = Xtilde⁴ = X⁴ there — no fourth-root ambiguity survives the fourth power.
4. The identity spreads to all of Region by the identity theorem (AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq on the half-plane {5/4 < Im z}, on which both sides are holomorphic since ‖J‖ > 1 there).

The only limit that is not pure soft analysis is Ytilde → 5/144, and even it needs no new estimates: by D E₄ = q·Φ′(q) (normalizedDeriv_eq_q_mul_deriv_cuspFunction) with Φ′(0) = 240 (E₄_qExpansion_coeff_one), and Δ/q = kfun → 1 (from lemk), (E₂E₄-E₆)/(E₄³-E₆²) = 3qΦ′(q)/(1728·q·kfun) → 720/1728 = 5/12.

The two solution pairs, at the level of ℂ

Elementary algebra around 1/J

Derivatives of the Eisenstein series at the ℂ-level

These repackage the Ramanujan identities deriv_comp_ofComplex_E2/E₄/E₆ as HasDerivAt statements for the compositions with ofComplex, ready for the chain rule.

The linear 2×2 system satisfied by both pairs

Limits of the two pairs at i∞

All limits are soft consequences of E₂, E₄, E₆ → 1 except Ytilde → 5/144, which uses the cusp-function factorization of D E₄ and kfun → 1.

Small helpers for the "eventually" bookkeeping

The vertical-line Wronskian argument

theorem Chudnovsky.E₄_eq_hyp2F1_pow_four {τ : UpperHalfPlane} (hτ : τ ∈ Region) : ModularForm.E₄ τ = hyp2F1 (J τ)⁻¹ ^ 4

Kummer's solution for the lattice Ltilde = Δ^(1/12)·L_τ (paper Thm. omegastrich, ch. 8), in the branch-free fourth-power form recommended by PLAN A7: for all τ with Im τ > 1.25, E₄(τ) = (₂F₁(1/12, 5/12; 1; 1/J(τ)))⁴.

This is equivalent to the paper's Δ(τ)^(1/12) = (2π/12^(1/4)) · J(τ)^(-1/12) · ₂F₁(1/12, 5/12; 1; 1/J(τ)) raised to the 12th power (see the module docstring), with the branch fixed as the paper does in its Main Theorem via continuity/connectedness on Region.