Viazovska's Magic Function — Original Contour Integrals

This file defines the magic function a(r) from Viazovska's proof of the optimality of the E₈ sphere packing [Via2017] and proves the key contour equivalence I₁₂ = I₁₂_vert + I₁₂_horiz (rectangular decomposition of the diagonal contour from -1 to i).

What we prove

The function aRad(r) is defined using the original triangular contours from Viazovska's paper:

aRad(r) = ∫_{-1→i} φ₀(-1/(z+1)) · (z+1)² · e^{πirz} dz
         + ∫_{1→i}  φ₀(-1/(z-1)) · (z-1)² · e^{πirz} dz
         - 2 ∫_{0→i} φ₀(-1/z) · z² · e^{πirz} dz
         + 2 ∫_{i→i∞} φ₀(z) · e^{πirz} dz

where φ₀(z) = (E₂E₄ - E₆)² / Δ(z).

The main result I12_eq_rectangular proves that the diagonal contour integral ∫_{-1→i} equals the sum of a vertical integral ∫_{-1→-1+i} and a horizontal integral ∫_{-1+i→i}. This is the first step toward evaluating aRad(r) via the Fourier expansion of φ₀.

How this differs from Sphere-Packing-Lean (Gauss2 PR)

The Sphere-Packing-Lean formalization deforms the original triangular contours into rectangular contours from the start, avoiding the cusp singularity at z = -1, 0, 1 entirely. The contour integrals are then evaluated on rectangles where all four sides lie strictly inside the upper half-plane.

Our approach keeps Viazovska's original contours and handles the cusp singularities directly:

1. Holomorphicity of φ₀: We prove E₂ is holomorphic on ℍ via E₂ = (πI/12)⁻¹ · logDeriv(η) (Dedekind eta), then build up to φ₀'' holomorphic on ℍ (PhiHolomorphic.lean). The Gauss2 PR instead uses the Serre derivative and Ramanujan's identity E₂E₄ - E₆ = 3D(E₄).

2. Cusp decay: We prove φ₀ is bounded at Im → ∞ via the q-expansion bound |E₂E₄-E₆| ≤ K|q| (CuspDecay.lean), using |E₂-1| ≤ 192|q| from a comparison test on the Eisenstein series.

3. Contour equivalence: We prove I₁₂ = I₁₂_vert + I₁₂_horiz using path independence from holomorphic_convex_primitive on the convex upper half-plane. The proof takes a primitive G of the integrand, applies FTC to truncated integrals (starting at height δ > 0), then takes δ → 0 using the cusp cancellation (z+1)² → 0 at z = -1.

4. Infrastructure: The key tool is holomorphic_convex_primitive from GeneralizedResidueTheory/CauchyPrimitive.lean, which gives path independence for holomorphic functions on convex open sets. This is part of our broader generalized residue theorem framework (Hungerbühler-Wasem, Theorem 3.3), though this file only uses the convex primitive — the full generalized residue theorem and ContourCycle framework will be applied when computing aRad(r) via the S-transformation of φ₀.

Main results

• φ₀''_differentiableOn : φ₀ is holomorphic on ℍ
• continuousOn_diagonal_integrand : the parameterized diagonal integrand is continuous on [0,1] (including the cusp endpoint t = 0)
• continuousOn_vertical_integrand : same for the vertical parameterization
• I12_eq_rectangular : I₁₂(r) = I₁₂_vert(r) + I₁₂_horiz(r)

References

• Viazovska, M. S. (2017). "The sphere packing problem in dimension 8." Annals of Mathematics, 185(3), 991-1015.
• Hungerbühler, N., Wasem, M. (2019). "A generalized version of the residue theorem." arXiv:1808.00997v2.

Modular form ingredients

We use φ₀'' (the ℂ-extended version of φ₀) from Modularforms/Eisenstein.lean. This is defined as φ₀''(z) = φ₀(z) when Im(z) > 0, and 0 otherwise. The underlying φ₀(z) = (E₂E₄ - E₆)² / Δ(z) is defined on the upper half-plane ℍ.

Key properties (proven in Eisenstein.lean and Delta.lean):

• φ₀ is holomorphic on ℍ (since Δ ≠ 0 on ℍ)
• Periodic: φ₀(z+1) = φ₀(z)
• S-transform: φ₀(-1/z) = φ₀(z) - (12i/π)·(1/z)·φ₋₂(z) - (36/π²)·(1/z²)·φ₋₄(z)
• Vanishing: φ₀(z) = O(e^{-2πIm(z)}) as Im(z) → ∞

Original Viazovska contour integrals

The four integrals defining aRad(r), using straight-line contours from the real axis to i.

noncomputable def viazovskaIntegrandLeft (r : ℝ) (z : ℂ) : ℂ

The integrand for I₁+I₂: φ₀(-1/(z+1)) · (z+1)² · e^{πirz}. At z = -1 (the cusp), (z+1)² = 0 cancels the singularity of φ₀.

Equations

• viazovskaIntegrandLeft r z = φ₀'' (-1 / (z + 1)) * (z + 1) ^ 2 * Complex.exp (↑Real.pi * Complex.I * ↑r * z)

noncomputable def viazovskaIntegrandRight (r : ℝ) (z : ℂ) : ℂ

The integrand for I₃+I₄: φ₀(-1/(z-1)) · (z-1)² · e^{πirz}. At z = 1 (the cusp), (z-1)² = 0 cancels the singularity.

Equations

• viazovskaIntegrandRight r z = φ₀'' (-1 / (z - 1)) * (z - 1) ^ 2 * Complex.exp (↑Real.pi * Complex.I * ↑r * z)

noncomputable def viazovskaIntegrandCenter (r : ℝ) (z : ℂ) : ℂ

The integrand for I₅: φ₀(-1/z) · z² · e^{πirz}. At z = 0 (the cusp), z² = 0 cancels the singularity.

Equations

• viazovskaIntegrandCenter r z = φ₀'' (-1 / z) * z ^ 2 * Complex.exp (↑Real.pi * Complex.I * ↑r * z)

noncomputable def viazovskaIntegrandTail (r : ℝ) (z : ℂ) : ℂ

The integrand for I₆: φ₀(z) · e^{πirz}. No singularity issues (Im(z) ≥ 1 on the contour).

Equations

• viazovskaIntegrandTail r z = φ₀'' z * Complex.exp (↑Real.pi * Complex.I * ↑r * z)

def contourNeg1ToI (t : ℝ) : ℂ

The straight-line contour from -1 to i (original Viazovska path).

Equations

• contourNeg1ToI t = -1 + (1 + Complex.I) * ↑t

def contour1ToI (t : ℝ) : ℂ

The straight-line contour from 1 to i (original Viazovska path).

Equations

• contour1ToI t = 1 + (-1 + Complex.I) * ↑t

def contour0ToI (t : ℝ) : ℂ

The straight-line contour from 0 to i (vertical segment).

Equations

• contour0ToI t = Complex.I * ↑t

The magic function aRad(r)

Defined using the original Viazovska contours.

noncomputable def I12 (r : ℝ) : ℂ

I₁₂(r) = ∫_{-1}^{i} φ₀(-1/(z+1)) · (z+1)² · e^{πirz} dz

Equations

• I12 r = ∫ (t : ℝ) in 0..1, viazovskaIntegrandLeft r (contourNeg1ToI t) * deriv contourNeg1ToI t

noncomputable def I34 (r : ℝ) : ℂ

I₃₄(r) = ∫_{1}^{i} φ₀(-1/(z-1)) · (z-1)² · e^{πirz} dz

Equations

• I34 r = ∫ (t : ℝ) in 0..1, viazovskaIntegrandRight r (contour1ToI t) * deriv contour1ToI t

noncomputable def I5 (r : ℝ) : ℂ

I₅(r) = -2 ∫_{0}^{i} φ₀(-1/z) · z² · e^{πirz} dz

Equations

• I5 r = -2 * ∫ (t : ℝ) in 0..1, viazovskaIntegrandCenter r (contour0ToI t) * deriv contour0ToI t

noncomputable def I6 (r : ℝ) : ℂ

I₆(r) = 2 ∫_{i}^{i∞} φ₀(z) · e^{πirz} dz (the semi-infinite vertical integral).

Equations

• I6 r = 2 * ∫ (t : ℝ) in Set.Ici 1, viazovskaIntegrandTail r (Complex.I * ↑t) * Complex.I

noncomputable def aRad (r : ℝ) : ℂ

The radial magic function aRad(r) from Viazovska [Via2017].

Equations

• aRad r = I12 r + I34 r + I5 r + I6 r

Holomorphicity of φ₀

φ₀ = (E₂·E₄ - E₆)² / Δ is holomorphic on ℍ because:

• E₂ is holomorphic (proved in PhiHolomorphic.lean via E₂ = const · logDeriv(η))
• E₄, E₆ are modular forms (holomorphic by .holo')
• Δ is a cusp form (holomorphic) and Δ ≠ 0 on ℍ
• Products, differences, squares, and ratios of holomorphic functions (with nonzero denominator) are holomorphic

theorem φ₀''_differentiableOn : DifferentiableOn ℂ φ₀'' {z : ℂ | 0 < z.im}

φ₀'' is holomorphic on the upper half-plane.

Upper half-plane: convexity and openness

theorem isOpen_upperHalfPlaneSet : IsOpen UpperHalfPlane.upperHalfPlaneSet

Alias of UpperHalfPlane.isOpen_upperHalfPlaneSet.

theorem convex_upperHalfPlaneSet : Convex ℝ {z : ℂ | 0 < z.im}

The upper half-plane {z : ℂ | 0 < z.im} is convex.

Holomorphicity of the integrand

theorem neg_inv_add_one_im_pos {z : ℂ} (hz : 0 < z.im) : 0 < (-1 / (z + 1)).im

When Im(z) > 0, the point -1/(z+1) also has positive imaginary part.

theorem viazovska_integrand_left_differentiableOn (r : ℝ) : DifferentiableOn ℂ (viazovskaIntegrandLeft r) {z : ℂ | 0 < z.im}

The integrand viazovskaIntegrandLeft r is holomorphic on the upper half-plane. This follows from holomorphicity of φ₀'' and the algebraic factors.

Contour equivalence infrastructure

Segment integrals and the fundamental theorem of calculus

Given a holomorphic function f on a convex open set S with primitive G (i.e., G' = f on S), the segment integral from a to b equals G(b) - G(a). This gives path independence: for a, b, c ∈ S,

∫_{a→b} f dz = ∫_{a→c} f dz + ∫_{c→b} f dz

since both sides equal G(b) - G(a).

theorem segment_integral_eq_sub_of_hasDerivAt {f G : ℂ → ℂ} {S : Set ℂ} (_hS_open : IsOpen S) (hS_convex : Convex ℝ S) {a b : ℂ} (ha : a ∈ S) (hb : b ∈ S) (hG : ∀ z ∈ S, HasDerivAt G (f z) z) (hf_cont : ContinuousOn f S) : ∫ (t : ℝ) in 0..1, f (a + t • (b - a)) * (b - a) = G b - G a

FTC for segment integrals: if G' = f on a convex open set, then the segment integral of f from a to b equals G(b) - G(a).

theorem segment_integral_add_of_holomorphic {f : ℂ → ℂ} {S : Set ℂ} (hS_open : IsOpen S) (hS_convex : Convex ℝ S) (hf : DifferentiableOn ℂ f S) {a b c : ℂ} (ha : a ∈ S) (hb : b ∈ S) (hc : c ∈ S) : ∫ (t : ℝ) in 0..1, f (a + t • (b - a)) * (b - a) = (∫ (t : ℝ) in 0..1, f (a + t • (c - a)) * (c - a)) + ∫ (t : ℝ) in 0..1, f (c + t • (b - c)) * (b - c)

Contour additivity: for a holomorphic function on a convex open set, the segment integral from a to b equals the sum of segment integrals from a to c and from c to b.

Contour parameterization lemmas

theorem deriv_contour_neg1_to_i (t : ℝ) : deriv contourNeg1ToI t = 1 + Complex.I

The derivative of contourNeg1ToI is the constant 1 + I.

theorem I12_eq_segment_integral (r : ℝ) : I12 r = ∫ (t : ℝ) in 0..1, viazovskaIntegrandLeft r (-1 + t • (Complex.I - -1)) * (Complex.I - -1)

I12 expressed as a segment integral from -1 to I.

Rectangular decomposition integrals

noncomputable def I12Vert (r : ℝ) : ℂ

The vertical integral from -1 to -1+I: left side of the rectangular path.

Equations

• I12Vert r = ∫ (t : ℝ) in 0..1, viazovskaIntegrandLeft r (-1 + Complex.I * ↑t) * Complex.I

noncomputable def I12Horiz (r : ℝ) : ℂ

The horizontal integral from -1+I to I: top side of the rectangular path.

Equations

• I12Horiz r = ∫ (t : ℝ) in 0..1, viazovskaIntegrandLeft r (-1 + Complex.I + ↑t)

theorem I12_vert_eq_segment (r : ℝ) : I12Vert r = ∫ (t : ℝ) in 0..1, viazovskaIntegrandLeft r (-1 + t • (-1 + Complex.I - -1)) * (-1 + Complex.I - -1)

I12Vert expressed as a segment integral from -1 to -1+I.

theorem I12_horiz_eq_segment (r : ℝ) : I12Horiz r = ∫ (t : ℝ) in 0..1, viazovskaIntegrandLeft r (-1 + Complex.I + t • (Complex.I - (-1 + Complex.I))) * (Complex.I - (-1 + Complex.I))

I12Horiz expressed as a segment integral from -1+I to I.

Truncated contour equivalence

For δ > 0, the diagonal integral from -1 + δI to I equals the vertical integral from -1 + δI to -1 + I plus the horizontal integral from -1 + I to I. All three segments lie in the upper half-plane, so path independence (from holomorphic_convex_primitive) applies.

theorem neg_one_add_delta_I_mem_uhp {δ : ℝ} (hδ : 0 < δ) : -1 + ↑δ * Complex.I ∈ {z : ℂ | 0 < z.im}

The point -1 + δI lies in the upper half-plane for δ > 0.

theorem neg_one_add_I_mem_uhp : -1 + Complex.I ∈ {z : ℂ | 0 < z.im}

The point -1 + I lies in the upper half-plane.

theorem I_mem_uhp : Complex.I ∈ {z : ℂ | 0 < z.im}

The point I lies in the upper half-plane.

theorem truncated_contour_equivalence (r δ : ℝ) (hδ : 0 < δ) : have a := -1 + ↑δ * Complex.I; have c := -1 + Complex.I; have b := Complex.I; have F := viazovskaIntegrandLeft r; ∫ (t : ℝ) in 0..1, F (a + t • (b - a)) * (b - a) = (∫ (t : ℝ) in 0..1, F (a + t • (c - a)) * (c - a)) + ∫ (t : ℝ) in 0..1, F (c + t • (b - c)) * (b - c)

Truncated contour equivalence: for δ > 0, the diagonal segment integral from -1 + δI to I equals the vertical from -1 + δI to -1 + I plus the horizontal from -1 + I to I. This is path independence for holomorphic functions on the convex open upper half-plane.

theorem truncated_horiz_eq_I12_horiz (r : ℝ) : ∫ (t : ℝ) in 0..1, viazovskaIntegrandLeft r (-1 + Complex.I + t • (Complex.I - (-1 + Complex.I))) * (Complex.I - (-1 + Complex.I)) = I12Horiz r

The horizontal part of the truncated equivalence equals I12Horiz. The segment from -1+I to I does not depend on δ.

Path-specific cusp decay

Along the diagonal contour t -> -1 + t(1+I) and the vertical contour t -> -1 + tI, as t -> 0+ the substitution w = -1/(z+1) sends Im(w) -> +infty. So phi0_isBoundedAtImInfty gives a bound on phi_0(w), and the (z+1)^2 = O(t^2) factor drives the integrand to 0.

Step 5: Cusp decay and integrand boundary behavior

To pass from the truncated contour equivalence (δ > 0) to the full equivalence (starting at -1), we need the integrand to vanish at z = -1. This follows from the cusp behavior of φ₀: as z → -1, the substitution w = -1/(z+1) sends Im(w) → +∞, and the q-expansion of φ₀ shows φ₀(w) = O(e^{-2πIm(w)}). The factor (z+1)² cancels the 1/w² from the change of variables, leaving the integrand → 0.

We state the key cusp estimates as sorry'd lemmas (requiring q-expansion infrastructure) and prove the contour equivalence from them.

The general statement Tendsto (viazovskaIntegrandLeft r) (𝓝[ℍ] (-1)) (𝓝 0) requires T-periodicity of φ₀ and compactness arguments on the fundamental domain. Since the main theorem I12_eq_rectangular uses a direct bound on the connecting segment (where Im(w) ≥ 1/(2δ) → ∞) via phi0_isBoundedAtImInfty, this general tendsto is not needed.

Helpers for cusp-decay continuity at t = 0

Both continuousOn_diagonal_integrand and continuousOn_vertical_integrand need an epsilon-delta squeeze at t = 0 using phi0_isBoundedAtImInfty. We factor out the common sub-arguments into reusable helpers.

theorem continuousOn_diagonal_integrand (r : ℝ) : ContinuousOn (fun (t : ℝ) => viazovskaIntegrandLeft r (contourNeg1ToI t) * (1 + Complex.I)) (Set.Icc 0 1)

The parameterized diagonal integrand is continuous on [0,1].

theorem continuousOn_vertical_integrand (r : ℝ) : ContinuousOn (fun (t : ℝ) => viazovskaIntegrandLeft r (-1 + Complex.I * ↑t) * Complex.I) (Set.Icc 0 1)

The parameterized vertical integrand is continuous on [0,1].

Step 5b: FTC-based limit argument

The key observation is that all segment integrals equal G(endpoint) - G(startpoint) for a primitive G on the upper half-plane. As δ → 0, the starting point -1 + δI approaches -1, and G(-1 + δI) converges by continuity.

We work with the primitive directly to avoid dominated convergence.

theorem exists_primitive_viazovska_integrand_left (r : ℝ) : ∃ (G : ℂ → ℂ), ∀ z ∈ {z : ℂ | 0 < z.im}, HasDerivAt G (viazovskaIntegrandLeft r z) z

The primitive G of viazovskaIntegrandLeft r on the upper half-plane, whose existence follows from holomorphic_convex_primitive.

theorem truncated_diagonal_eq_primitive_sub (r : ℝ) (G : ℂ → ℂ) (hG : ∀ z ∈ {z : ℂ | 0 < z.im}, HasDerivAt G (viazovskaIntegrandLeft r z) z) (δ : ℝ) (hδ : 0 < δ) : ∫ (t : ℝ) in 0..1, viazovskaIntegrandLeft r (-1 + ↑δ * Complex.I + t • (Complex.I - (-1 + ↑δ * Complex.I))) * (Complex.I - (-1 + ↑δ * Complex.I)) = G Complex.I - G (-1 + ↑δ * Complex.I)

The truncated diagonal integral from -1 + δI to I equals G(I) - G(-1+δI) for the primitive G of the integrand.

theorem truncated_vertical_eq_primitive_sub (r : ℝ) (G : ℂ → ℂ) (hG : ∀ z ∈ {z : ℂ | 0 < z.im}, HasDerivAt G (viazovskaIntegrandLeft r z) z) (δ : ℝ) (hδ : 0 < δ) : ∫ (t : ℝ) in 0..1, viazovskaIntegrandLeft r (-1 + ↑δ * Complex.I + t • (-1 + Complex.I - (-1 + ↑δ * Complex.I))) * (-1 + Complex.I - (-1 + ↑δ * Complex.I)) = G (-1 + Complex.I) - G (-1 + ↑δ * Complex.I)

The truncated vertical integral from -1 + δI to -1 + I equals G(-1+I) - G(-1+δI) for the primitive.

theorem horizontal_eq_primitive_sub (r : ℝ) (G : ℂ → ℂ) (hG : ∀ z ∈ {z : ℂ | 0 < z.im}, HasDerivAt G (viazovskaIntegrandLeft r z) z) : I12Horiz r = G Complex.I - G (-1 + Complex.I)

The horizontal integral from -1 + I to I equals G(I) - G(-1+I).

Step 6: Full contour equivalence via primitive cancellation

The full contour equivalence I12 = I12Vert + I12Horiz follows from the primitive approach: both sides equal G(I) - lim_{δ→0} G(-1+δI).

The truncated versions give:

• Diagonal: G(I) - G(-1+δI)
• Vertical + Horizontal: (G(-1+I) - G(-1+δI)) + (G(I) - G(-1+I)) = G(I) - G(-1+δI)

So truncated diagonal = truncated vertical + horizontal for all δ > 0. Taking δ → 0 and using continuity of the integrals gives the result.

theorem I12_split_at_delta (r δ : ℝ) (hδ₀ : 0 ≤ δ) (hδ₁ : δ ≤ 1) (hcont : ContinuousOn (fun (t : ℝ) => viazovskaIntegrandLeft r (contourNeg1ToI t) * (1 + Complex.I)) (Set.Icc 0 1)) : I12 r = (∫ (t : ℝ) in 0..δ, viazovskaIntegrandLeft r (contourNeg1ToI t) * (1 + Complex.I)) + ∫ (t : ℝ) in δ..1, viazovskaIntegrandLeft r (contourNeg1ToI t) * (1 + Complex.I)

I12 equals the integral restricted to [δ, 1] plus the integral on [0, δ]. For continuous integrands (from continuousOn_diagonal_integrand), the [0, δ] part vanishes as δ → 0.

theorem I12_vert_split_at_delta (r δ : ℝ) (hδ₀ : 0 ≤ δ) (hδ₁ : δ ≤ 1) (hcont : ContinuousOn (fun (t : ℝ) => viazovskaIntegrandLeft r (-1 + Complex.I * ↑t) * Complex.I) (Set.Icc 0 1)) : I12Vert r = (∫ (t : ℝ) in 0..δ, viazovskaIntegrandLeft r (-1 + Complex.I * ↑t) * Complex.I) + ∫ (t : ℝ) in δ..1, viazovskaIntegrandLeft r (-1 + Complex.I * ↑t) * Complex.I

I12Vert equals the integral restricted to [δ, 1] plus the integral on [0, δ].

Helpers for I12_eq_rectangular

The proof of I12_eq_rectangular decomposes into:

1. Chain rule / FTC for tail integrals
2. An algebraic identity expressing the difference as three small terms
3. Each of those three terms tending to zero as delta -> 0+
4. Tendsto uniqueness to conclude

theorem I12_eq_rectangular (r : ℝ) : I12 r = I12Vert r + I12Horiz r

Full contour equivalence: the diagonal integral I12 from -1 to I equals the sum of the vertical integral I12Vert (from -1 to -1+I) and the horizontal integral I12Horiz (from -1+I to I).

Summary of sorry dependencies

Remaining sorry'd lemmas:

All sorries have been filled:

• phi0_bounded_at_infty — via CuspDecay.lean import
• continuousOn_diagonal_integrand — direct squeeze bound using phi0_isBoundedAtImInfty
• continuousOn_vertical_integrand — same pattern as diagonal
• I12_eq_rectangular — primitive + FTC + limit argument, with direct segment bound (avoids viazovska_integrand_left_tendsto_zero by bounding φ₀ on the connecting segment where Im(w) ≥ 1/(2δ) → ∞)