Prove2Me

Horizontal norm relation for seeded theta elements

Open
HorizontalPadicL.seededFiniteThetaElements_normRelation

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

modular-formsmodular-symbolsnumber-theoryp-adic-l-functions

The Hecke distribution relation for modular symbols implies that projection after adjoining one auxiliary prime multiplies the finite theta element by the corresponding horizontal Euler factor.

Deprecated. SeededFiniteThetaData stores arbitrary theta and eulerFactor functions and does not assert that they arise from modular symbols, so the universal statement for an arbitrary Θ is false. Use HorizontalPadicL.seededFiniteThetaElements_exist_with_normRelation (0baaf1f7-18a1-4956-9c6f-a09088f3283d), which constructs the theta elements and proves their norm relations simultaneously.

Preamble
import Definitions.Def_KN_SeededThetaConstruction

set_option autoImplicit false
noncomputable section
Formal statement
namespace HorizontalPadicL

/-- The distribution relation for modular symbols gives the horizontal norm
relation for the unnormalised theta elements. This is the substantive input
from Kriz--Nordentoft, Section 3. -/
theorem seededFiniteThetaElements_normRelation
    {N k p B : ℕ} {ι : MTT.Qbar →+* ℂ} [Fact p.Prime]
    (hN : 0 < N) (hk : 2 ≤ k) (heven : Even k)
    (f : MTT.Eigenform N k ι) (hnew : IsNewEigenform f)
    (P : MTT.Periods k ι f.form) (η : DirichletCharacterWithLevel)
    (hηprim : η.2.IsPrimitive) (hηeven : η.2 (-1) = 1)
    (ιp : MTT.Qbar →+* ℂ_[p])
    (L : SeededHorizontalPrimeDataV2 p ιp f η B)
    (Θ : SeededFiniteThetaData L) :
    Θ.SatisfiesNormRelations := by sorry

end HorizontalPadicL
Source
Kriz--Nordentoft, https://arxiv.org/pdf/2310.20678, Proposition 3.5 and Corollary 3.6.

View graph