Cusp decay of mixed-period test functions

Open

MTT.Cohomology.mixed_period_test_functions_cusp_decay

by davidloeffler · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

cohomologycomplex-analysismodular-forms

For the two canonical scalar contractions built from a mixed-period primitive $U$ and a cusp form $q$ , every weight-normalized translate tends to zero at the infinite cusp. The assertion expresses that the exponential decay of a cusp form dominates the polynomial growth allowed for $U$ in every cusp chart.

Retired. This statement omits the necessary positive-level hypothesis $0<N$ . Use MTT.Cohomology.mixed_period_test_functions_cusp_decay_of_pos_level, which explicitly assumes $N>0$ and $k\ge2$ .

Preamble

import Definitions.Def_MTT_PeriodPairing
import Mathlib.NumberTheory.ModularForms.Bounds

set_option autoImplicit false
noncomputable section
open UpperHalfPlane MeasureTheory
open scoped MatrixGroups Modular ComplexConjugate
open MTT.Cohomology

Formal statement

theorem MTT.Cohomology.mixed_period_test_functions_cusp_decay
    {N k : ℕ} (hk : 2 ≤ k)
    (g v q : CuspForm (MTT.GammaOne N) (k : ℤ))
    (U : ℂ → Binary ℂ) (hU : IsMixedPeriodPrimitive g v U) :
    let A₁ : ℂ → ℂ := fun z =>
      periodContraction (k - 2) (U z)
        (conj ((↑ₕ(fun τ : ℍ ↦ q τ)) z) • periodPower (k - 2) (conj z))
    let A₂ : ℂ → ℂ := fun z => conj <|
      periodContraction (k - 2)
        (((↑ₕ(fun τ : ℍ ↦ q τ)) z) • periodPower (k - 2) z) (U z)
    (∀ σ : Matrix.SpecialLinearGroup (Fin 2) ℤ, IsZeroAtImInfty
      fun τ : ℍ ↦ A₁ ((σ • τ : ℍ) : ℂ) *
        ((starRingEnd ℂ (denom σ τ)) ^ 2)⁻¹) ∧
    (∀ σ : Matrix.SpecialLinearGroup (Fin 2) ℤ, IsZeroAtImInfty
      fun τ : ℍ ↦ A₂ ((σ • τ : ℍ) : ℂ) *
        ((starRingEnd ℂ (denom σ τ)) ^ 2)⁻¹) := by sorry

Source

Classical mixed Eichler--Shimura period pairing argument: contraction invariance, Wirtinger differentiation, and exponential decay of cusp forms.

View graph