The Main Theorem (Milla, ch. 9)

The paper's ch. 9: the differential-equation form thm42 and the Main Theorem hauptformel,

1/(2π·Im τ) · √(J(τ)/(J(τ)−1))
  = ∑ n, ((1−s₂(τ))/6 + n) · (6n)!/((3n)!(n!)³) · (1728·J(τ))⁻ⁿ    (Im τ > 1.25)

where √ is the principal branch (here: Complex.cpow (1/2)).

The intermediate propositions thm35 (quasiperiod/period derivative relation) and thmglg10 (η₁ − (3g₃/2g₂)s₂ = π/Im τ) are stated in lattice language in the paper; here the whole ch. 9 computation is carried out in modular language, replacing the quasiperiod calculus by Ramanujan's derivative identities (Ramanujan.lean) applied to Kummer's identity E₄ = ₂F₁(1/12,5/12;1;1/J)⁴ (Kummer.lean): see the section "The proof of thm42" below.

The branch of the square root is resolved pointwise in thm42: J/(J−1) = (G⁶/E₆)² with Re(G⁶/E₆) > 0 everywhere on Region (by explicit estimates), and the principal square root of w² is w on the right half-plane (Complex.sq_cpow_two_inv). The connectedness workhorse sq_eq_on_preconnected_eq originally planned for this step (PLAN A8) is kept for reference/reuse.

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

Gsq z = (₂F₁(1/12, 5/12; 1; z))², the square of Kummer's solution (the function G in the proof of the Main Theorem).

Equations

• Chudnovsky.Gsq z = ₂F₁ (1 / 12) (5 / 12) 1 z ^ 2

noncomputable def Chudnovsky.mainSummand (τ : UpperHalfPlane) (n : ℕ) : ℂ

The summand of the Main Theorem's series: ((1−s₂(τ))/6 + n) · (6n)!/((3n)!(n!)³) · (1728·J(τ))⁻ⁿ.

Equations

• Chudnovsky.mainSummand τ n = ((1 - Chudnovsky.s₂ τ) / 6 + ↑n) * (↑(6 * n).factorial / (↑(3 * n).factorial * ↑n.factorial ^ 3)) / (1728 * Chudnovsky.J τ) ^ n

theorem Chudnovsky.summable_mainSummand {τ : UpperHalfPlane} (hτ : τ ∈ Region) : Summable (mainSummand τ)

The Main Theorem's series converges absolutely on the region Im τ > 1.25 (ratio test: (6n)!/((3n)!(n!)³) ≤ 1728ⁿ and ‖1728·J‖ > 1728 on the region).

theorem Chudnovsky.sq_eq_on_preconnected_eq {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsPreconnected s) {f g : X → ℂ} (hf : ContinuousOn f s) (hg : ContinuousOn g s) (hfg : ∀ x ∈ s, f x ^ 2 = g x ^ 2) (hg0 : ∀ x ∈ s, g x ≠ 0) {x₀ : X} (hx₀ : x₀ ∈ s) (h₀ : f x₀ = g x₀) (x : X) : x ∈ s → f x = g x

The branch-resolution workhorse (PLAN A8): two continuous functions on a preconnected set whose squares agree, the second nonvanishing, agreeing at one point, agree everywhere.

theorem Chudnovsky.isPreconnected_Region : IsPreconnected Region

The region Im τ > 1.25 is preconnected.

The reduction hauptformel ← thm42

Milla's derivation of the Main Theorem from thm42 is the term-by-term differentiation of the series darst (hyp2F1_sq_eq_tsum): with cₙ = (6n)!/((3n)!(n!)³·1728ⁿ) and w = 1/J (so ‖w‖ < 1 on the region), (1−s₂)/6·G(w) + w·G′(w) = ∑ ((1−s₂)/6 + n)·cₙ·wⁿ = ∑ mainSummand.

The proof of thm42

Following the modular-forms reformulation of the paper's ch. 9 computation: with G = ₂F₁(1/12,5/12;1;1/J) (so E₄ = G⁴ by Kummer's Thm. omegastrich), Ramanujan's identity D E₄ = (E₂E₄−E₆)/3 and the derivative D J = −J·E₆/E₄ (from D E₄, D E₆) combine via the chain rule to E₂ = E₆/E₄ + 12G³G′E₆/(E₄²J). Substituting this and E₄ = G⁴ into the right-hand side of thm42 collapses it to G⁶/(2πE₆·Im τ); and the left-hand side equals the same value because J/(J−1) = E₄³/E₆² = (G⁶/E₆)² and the principal square root of w² is w whenever Re w > 0 — which holds here by the explicit estimates ‖G²−1‖ ≤ 0.15 (from the Gsq power series, ‖1/J‖ < 1/1.096) and ‖E₆−1‖ ≤ 0.199 (from Estimates.lean). This replaces the paper's continuity/connectedness branch argument by a pointwise right-half-plane one.

theorem Chudnovsky.thm42 {τ : UpperHalfPlane} (hτ : τ ∈ Region) : 1 / (2 * ↑Real.pi * ↑τ.im) * (J τ / (J τ - 1)) ^ (1 / 2) = (1 - s₂ τ) / 6 * Gsq (1 / J τ) + 1 / J τ * deriv Gsq (1 / J τ)

Milla's Prop. thm42: the differential equation 1/(2π·Im τ)·√(J/(J−1)) = (1−s₂)/6 · G(1/J) + (1/J)·G′(1/J) for Im τ > 1.25, with the principal branch of the square root. The branch is resolved pointwise: J/(J−1) = (G⁶/E₆)² with Re(G⁶/E₆) > 0 on all of Region (by the explicit estimates), and the principal square root of w² is w on the right half-plane.

theorem Chudnovsky.hauptformel {τ : UpperHalfPlane} (hτ : τ ∈ Region) : 1 / (2 * ↑Real.pi * ↑τ.im) * (J τ / (J τ - 1)) ^ (1 / 2) = ∑' (n : ℕ), mainSummand τ n

The Main Theorem (Milla, Thm. hauptformel; Chudnovsky–Chudnovsky 1988, Eq. (1.4)): for all τ with Im τ > 1.25, 1/(2π·Im τ)·√(J/(J−1)) = ∑ n, ((1−s₂)/6 + n)·(6n)!/((3n)!(n!)³)·(1728·J)⁻ⁿ, with the principal branch of the square root.