Asymptotic Behavior of Eisenstein Series

This file establishes the asymptotic behavior of Eisenstein series as z → i∞, and constructs the ModularForm structures for Serre derivatives.

Main definitions

• serre_DE₄_ModularForm, serre_DE₆_ModularForm, serre_DE₂_ModularForm : Package serre derivatives as modular forms

Main results

• D_tendsto_zero_of_tendsto_const : Cauchy estimate: D f → 0 at i∞ if f is bounded
• E₂_tendsto_one_atImInfty : E₂ → 1 at i∞
• serre_DE₄_tendsto_atImInfty, serre_DE₆_tendsto_atImInfty, serre_DE₂_tendsto_atImInfty : Limits of serre derivatives (for determining scalars)

Cauchy estimates and limits at infinity

theorem D_tendsto_zero_of_tendsto_const {f : UpperHalfPlane → ℂ} (hf : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) f) (hbdd : UpperHalfPlane.IsBoundedAtImInfty f) : Filter.Tendsto (D f) UpperHalfPlane.atImInfty (nhds 0)

If f is holomorphic and bounded at infinity, then D f → 0 at i∞.

Proof via Cauchy estimates: For z with large Im, consider the ball B(z, Im(z)/2) in ℂ.

• Ball is contained in upper half plane: all points have Im > Im(z)/2 > 0
• f ∘ ofComplex is holomorphic on the ball (from MDifferentiable)
• f is bounded by M for Im ≥ A (from IsBoundedAtImInfty)
• By Cauchy: |deriv(f ∘ ofComplex)(z)| ≤ M / (Im(z)/2) = 2M/Im(z)
• D f = (2πi)⁻¹ * deriv(...), so |D f(z)| ≤ M/(π·Im(z)) → 0

Limits of Eisenstein series at infinity

theorem tendsto_exp_neg_mul_atTop {c : ℝ} (hc : 0 < c) : Filter.Tendsto (fun (y : ℝ) => Real.exp (-c * y)) Filter.atTop (nhds 0)

exp(-c * y) → 0 as y → +∞ (for c > 0).

theorem tendsto_zero_of_exp_decay {f : UpperHalfPlane → ℂ} {c : ℝ} (hc : 0 < c) (hO : f =O[UpperHalfPlane.atImInfty] fun (τ : UpperHalfPlane) => Real.exp (-c * τ.im)) : Filter.Tendsto f UpperHalfPlane.atImInfty (nhds 0)

If f = O(exp(-c * Im z)) as z → i∞ for c > 0, then f → 0 at i∞.

theorem modular_form_tendsto_atImInfty {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) : Filter.Tendsto f.toFun UpperHalfPlane.atImInfty (nhds ((PowerSeries.coeff 0) (ModularFormClass.qExpansion 1 ⇑f)))

A modular form tends to its value at infinity as z → i∞.

theorem E₂_sub_one_isBigO_exp : (fun (z : UpperHalfPlane) => E₂ z - 1) =O[UpperHalfPlane.atImInfty] fun (z : UpperHalfPlane) => Real.exp (-(2 * Real.pi) * z.im)

E₂ - 1 = O(exp(-2π·Im z)) at infinity.

theorem E₂_tendsto_one_atImInfty : Filter.Tendsto E₂ UpperHalfPlane.atImInfty (nhds 1)

E₂ → 1 at i∞.

theorem E₄_tendsto_one_atImInfty : Filter.Tendsto E₄.toFun UpperHalfPlane.atImInfty (nhds 1)

E₄ → 1 at i∞.

theorem E₆_tendsto_one_atImInfty : Filter.Tendsto E₆.toFun UpperHalfPlane.atImInfty (nhds 1)

E₆ → 1 at i∞.

Boundedness lemmas

theorem E₆_isBoundedAtImInfty : UpperHalfPlane.IsBoundedAtImInfty E₆.toFun

E₆ is bounded at infinity (as a modular form).

theorem serre_DE₂_isBoundedAtImInfty : UpperHalfPlane.IsBoundedAtImInfty (serre_D 1 E₂)

serre_D 1 E₂ is bounded at infinity.

theorem DE₄_isBoundedAtImInfty : UpperHalfPlane.IsBoundedAtImInfty (D E₄.toFun)

D E₄ is bounded at infinity (by Cauchy estimate: D f → 0 when f is bounded).

theorem serre_DE₄_isBoundedAtImInfty : UpperHalfPlane.IsBoundedAtImInfty (serre_D 4 E₄.toFun)

serre_D 4 E₄ is bounded at infinity.

Construction of ModularForm from serre_D

def serre_DE₄_ModularForm : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) 6

serre_D 4 E₄ is a weight-6 modular form.

Equations

• serre_DE₄_ModularForm = serre_D_ModularForm 4 E₄

theorem serre_DE₆_isBoundedAtImInfty : UpperHalfPlane.IsBoundedAtImInfty (serre_D 6 E₆.toFun)

serre_D 6 E₆ is bounded at infinity.

def serre_DE₆_ModularForm : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) 8

serre_D 6 E₆ is a weight-8 modular form.

Equations

• serre_DE₆_ModularForm = serre_D_ModularForm 6 E₆

Limit of serre_D at infinity (for determining scalar)

theorem serre_D_tendsto_of_tendsto (k : ℤ) (f : UpperHalfPlane → ℂ) (c : ℂ) (hf_holo : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) f) (hf_bdd : UpperHalfPlane.IsBoundedAtImInfty f) (hf_lim : Filter.Tendsto f UpperHalfPlane.atImInfty (nhds c)) : Filter.Tendsto (serre_D (↑k) f) UpperHalfPlane.atImInfty (nhds (-↑k * c / 12))

General limit: if f → c at i∞ and f is holomorphic and bounded, then serre_D k f → -k*c/12.

This is the continuous mapping theorem applied to serre_D k f = D f - (k/12) * E₂ * f:

• D f → 0 (Cauchy estimate from boundedness)
• E₂ → 1
• f → c Therefore serre_D k f → 0 - (k/12) * 1 * c = -k*c/12.

theorem serre_D_tendsto_neg_k_div_12 (k : ℤ) (f : UpperHalfPlane → ℂ) (hf_holo : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) f) (hf_bdd : UpperHalfPlane.IsBoundedAtImInfty f) (hf_lim : Filter.Tendsto f UpperHalfPlane.atImInfty (nhds 1)) : Filter.Tendsto (serre_D (↑k) f) UpperHalfPlane.atImInfty (nhds (-↑k / 12))

Special case: if f → 1 at i∞, then serre_D k f → -k/12.

theorem serre_D_tendsto_zero_of_tendsto_zero (k : ℤ) (f : UpperHalfPlane → ℂ) (hf_holo : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) f) (hf_bdd : UpperHalfPlane.IsBoundedAtImInfty f) (hf_lim : Filter.Tendsto f UpperHalfPlane.atImInfty (nhds 0)) : Filter.Tendsto (serre_D (↑k) f) UpperHalfPlane.atImInfty (nhds 0)

Special case: if f → 0 at i∞, then serre_D k f → 0.

theorem serre_DE₄_tendsto_atImInfty : Filter.Tendsto (serre_D 4 E₄.toFun) UpperHalfPlane.atImInfty (nhds (-(1 / 3)))

serre_D 4 E₄ → -1/3 at i∞.

theorem serre_DE₆_tendsto_atImInfty : Filter.Tendsto (serre_D 6 E₆.toFun) UpperHalfPlane.atImInfty (nhds (-(1 / 2)))

serre_D 6 E₆ → -1/2 at i∞.

def serre_DE₂_ModularForm : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) 4

serre_D 1 E₂ is a weight-4 modular form. Note: E₂ itself is NOT a modular form, but serre_D 1 E₂ IS.

Equations

• serre_DE₂_ModularForm = { toFun := serre_D 1 E₂, slash_action_eq' := ⋯, holo' := serre_DE₂_ModularForm._proof_3, bdd_at_cusps' := @serre_DE₂_ModularForm._proof_4 }

theorem serre_DE₂_tendsto_atImInfty : Filter.Tendsto (serre_D 1 E₂) UpperHalfPlane.atImInfty (nhds (-(1 / 12)))

serre_D 1 E₂ → -1/12 at i∞.

Generic q-expansion summability and derivative bounds

theorem summable_pow_shift (k : ℕ) : Summable fun (m : ℕ) => (↑m + 1) ^ k * Real.exp (-2 * Real.pi * ↑m)

Summability of (m+1)^k * exp(-2πm) via comparison with shifted sum.

theorem qexp_deriv_bound_of_coeff_bound {a : ℕ+ → ℂ} {k : ℕ} (ha : ∀ (n : ℕ+), ‖a n‖ ≤ ↑↑n ^ k) (K : Set ℂ) : K ⊆ {w : ℂ | 0 < w.im} → IsCompact K → ∃ (u : ℕ+ → ℝ), Summable u ∧ ∀ (n : ℕ+) (z : ↑K), ‖a n * (2 * ↑Real.pi * Complex.I * ↑↑n) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑↑n * ↑z)‖ ≤ u n

Derivative bounds for q-expansion coefficients. Given ‖a n‖ ≤ n^k, produces bounds ‖a n * 2πin * exp(2πin z)‖ ≤ 2π * n^(k+1) * exp(-2πn * y_min) on compact K ⊆ {z : 0 < z.im}. This is a key hypothesis for D_qexp_tsum_pnat.