Unit norm-relation systems normalize to horizontal measures

Proved

HorizontalPadicL.unitNormRelationThetaSystem_to_normalizedMeasure

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

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

A finite horizontal theta system with unit transition factors can be normalized along a cofinal chain to give an exactly compatible measure. At every finite-order character its value differs from the original theta evaluation by a unit, so its critical-value zero set is unchanged.

Preamble

import Definitions.Def_KN_SeededFiniteThetaCriticalZeroSet

set_option autoImplicit false
noncomputable section

Formal statement

namespace HorizontalPadicL

/-- A finite theta system whose one-coordinate transition factors are units
can be normalized along a cofinal chain of finite subsets.  The resulting
compatible horizontal measure differs at every finite-order character from
the corresponding theta evaluation by a unit, and hence has the same zeroes. -/
theorem unitNormRelationThetaSystem_to_normalizedMeasure
    {N k p B : ℕ} {ι : MTT.Qbar →+* ℂ} [Fact p.Prime]
    {ιp : MTT.Qbar →+* ℂ_[p]} {f : MTT.Eigenform N k ι}
    {η : DirichletCharacterWithLevel}
    {L : SeededHorizontalPrimeDataV2 p ιp f η B}
    (Θ : SeededFiniteThetaDataV2 L)
    (hnorm : Θ.SatisfiesNormRelations)
    (hunit : Θ.HasUnitEulerFactors)
    (hzero : Θ.HasSeededCriticalZeroSet) :
    ∃ μ : SeededNormalizedThetaMeasureV2 L,
      μ.characters = Θ.characters ∧
      μ.InterpolatesSeededCriticalValues := by
  sorry

end HorizontalPadicL

Source

Standard inverse-limit normalization underlying Kriz--Nordentoft, Corollary 5.2 and Definition 5.3; https://arxiv.org/pdf/2310.20678.

View graph