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

• 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)

Limits of Eisenstein series at infinity

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) (UpperHalfPlane.qExpansion 1 ⇑f)))

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

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

E₂ → 1 at i∞: E₂ extends continuously to the cusp, with value the constant coefficient 1 of its q-expansion (mathlib's EisensteinSeries.hasSum_qExpansion_E2).

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₄.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 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.

Construction of ModularForm from serre_D

noncomputable 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₄

noncomputable 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 : MDiff 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 : MDiff 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 : MDiff 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∞.

noncomputable 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.