EisensteinAsymptotics

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

• serreDE₄ModularForm, serreDE₆ModularForm, serreDE₂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)

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) (UpperHalfPlane.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 (serreD 1 E₂)

serreD 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 (serreD 4 E₄.toFun)

serreD 4 E₄ is bounded at infinity.

Construction of ModularForm from serreD

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

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

Equations

• serreDE₄ModularForm = serreDModularForm 4 E₄

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

serreD 6 E₆ is bounded at infinity.

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

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

Equations

• serreDE₆ModularForm = serreDModularForm 6 E₆

Limit of serreD 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 (serreD (↑k) f) UpperHalfPlane.atImInfty (nhds (-↑k * c / 12))

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

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

• D f → 0 (Cauchy estimate from boundedness)
• E₂ → 1
• f → c Therefore serreD 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 (serreD (↑k) f) UpperHalfPlane.atImInfty (nhds (-↑k / 12))

Special case: if f → 1 at i∞, then serreD 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 (serreD (↑k) f) UpperHalfPlane.atImInfty (nhds 0)

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

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

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

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

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

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

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

Equations

• serreDE₂ModularForm = { toFun := serreD 1 E₂, slash_action_eq' := ⋯, holo' := serreDE₂ModularForm._proof_3, bdd_at_cusps' := @serreDE₂ModularForm._proof_4 }

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

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