Cusp decay for Eisenstein series and the Viazovska integrand

This file proves that the Eisenstein series E₄, E₆ tend to 1 at the cusp (Im -> infinity), and establishes key properties of the cuspFunction of Delta needed for cusp decay analysis.

Main results

• tendsto_qParam_atImInfty : qParam 1 z -> 0 as Im z -> infinity
• E₄_tendsto_one_atImInfty_SP : E₄ z -> 1 as Im z -> infinity
• E₆_tendsto_one_atImInfty_SP : E₆ z -> 1 as Im z -> infinity
• cF_Delta_div_q_tendsto : cuspFunction(Delta)(q)/q -> 1 as q -> 0
• tendsto_deriv_cF_Delta : (cuspFunction Delta)'(q) -> 1 as q -> 0
• cF_ratio_tendsto_one : q * cF'(q) / cF(q) -> 1 as q -> 0
• phi0_isBoundedAtImInfty : phi0 is bounded at Im -> infinity

Proof strategy for phi0_isBoundedAtImInfty

The function phi0(w) = (E2(w)*E4(w)-E6(w))^2 / Delta(w) is bounded at Im -> infinity. The proof chain is:

1. cF_ratio_tendsto_one: q * cF'(q)/cF(q) -> 1 (proven below)
2. logDeriv(Delta^24)(z) = 2*pi*I * cF'(q)/(cF(q)/q) via logDeriv_comp (chain rule)
3. logDeriv(eta^24) = 24 * logDeriv(eta) via logDeriv_fun_pow
4. logDeriv(eta)(z) = pi*I/12 * E2(z) via eta_logDeriv'
5. Combining: E2(z) = cF'(q)/(cF(q)/q) -> 1 as Im -> infinity
6. E2*E4 - E6 -> 1*1 - 1 = 0, so the numerator of phi0 vanishes
7. Combined with Delta = Theta(exp(-2*pi*Im)), phi0 is bounded

q-parameter and Eisenstein series at the cusp

theorem tendsto_qParam_atImInfty : Filter.Tendsto (fun (z : UpperHalfPlane) => Function.Periodic.qParam 1 ↑z) UpperHalfPlane.atImInfty (nhds 0)

The q-parameter q = exp(2*pi*i*z) tends to 0 as Im(z) -> infinity.

theorem E₄_tendsto_one_atImInfty_SP : Filter.Tendsto (⇑E₄) UpperHalfPlane.atImInfty (nhds 1)

E4(z) -> 1 as Im(z) -> infinity, from the q-expansion constant term.

theorem E₆_tendsto_one_atImInfty_SP : Filter.Tendsto (⇑E₆) UpperHalfPlane.atImInfty (nhds 1)

E6(z) -> 1 as Im(z) -> infinity, from the q-expansion constant term.

CuspFunction of Delta: analytic properties at q = 0

The cuspFunction cF(q) of Delta is analytic at q = 0 with cF(0) = 0 and cF'(0) = 1 (from the q-expansion Delta = q - 24*q^2 + ...). This gives cF(q)/q -> 1 and cF'(q) -> 1 as q -> 0.

noncomputable def cFDelta : ℂ → ℂ

The cuspFunction of Delta.

Equations

• cFDelta = UpperHalfPlane.cuspFunction 1 ⇑Delta

theorem deriv_cF_Delta_zero : deriv cFDelta 0 = 1

The derivative of cFDelta at 0 equals 1.

theorem cF_Delta_hasDerivAt_zero : HasDerivAt cFDelta 1 0

cFDelta has derivative 1 at 0.

theorem cF_Delta_div_q_tendsto : Filter.Tendsto (fun (q : ℂ) => cFDelta q / q) (nhdsWithin 0 {0}ᶜ) (nhds 1)

cF(q)/q -> 1 as q -> 0.

theorem continuousAt_deriv_cF_Delta : ContinuousAt (deriv cFDelta) 0

deriv cFDelta is continuous at 0.

theorem tendsto_deriv_cF_Delta : Filter.Tendsto (deriv cFDelta) (nhds 0) (nhds 1)

cF'(q) -> 1 as q -> 0.

theorem cF_ratio_tendsto_one : Filter.Tendsto (fun (q : ℂ) => q * deriv cFDelta q / cFDelta q) (nhdsWithin 0 {0}ᶜ) (nhds 1)

The ratio q * cF'(q) / cF(q) -> 1 as q -> 0 within q != 0.

phi0 is bounded at Im -> infinity

We prove φ₀ = (E₂E₄-E₆)²/Δ is bounded at Im -> infinity. The proof uses:

• E₂E₄-E₆ = (E₂-1)·E₄ + (E₄-E₆) is O(q) as Im → ∞
• |E₂-1| ≤ 192·|q| from the q-expansion series bound
• |E₄-E₆| ≤ L·|q| from analyticity of cuspFunctions
• |Δ| ≥ (1/2)|q| from cF_Delta_div_q_tendsto Combined: |φ₀| ≤ 2K²|q| → 0.

theorem phi0_isBoundedAtImInfty : UpperHalfPlane.IsBoundedAtImInfty φ₀

phi0 is bounded at Im -> infinity.