Normalized theta elements form a horizontal measure
OpenHorizontalPadicL.seededNormalizedThetaMeasure_existsmodular-formsmodular-symbolsnumber-theoryp-adic-l-functions
Dividing the finite theta elements by their unit Euler factors changes the norm relation into exact compatibility and hence produces a measure in the horizontal inverse limit.
Deprecated. This theorem returns a measure but records only equality of its character realization; it loses the fact that the measure was obtained by normalizing the supplied theta elements. That missing provenance prevents a sound later interpolation step. Use HorizontalPadicL.seededNormalizedThetaMeasure_exists_with_interpolation (1494c6fa-680a-46c2-b145-46387df6d7c1), which returns the constructed measure and its interpolation proof together.
Preamble
import Definitions.Def_KN_SeededThetaConstruction set_option autoImplicit false noncomputable section
Formal statement
namespace HorizontalPadicL
/-- Dividing the finite theta elements by the unit Euler factors converts their
norm relations into an exactly compatible inverse-limit measure. -/
theorem seededNormalizedThetaMeasure_exists
{N k p B : ℕ} {ι : MTT.Qbar →+* ℂ} [Fact p.Prime]
(f : MTT.Eigenform N k ι) (hnew : IsNewEigenform f)
(η : DirichletCharacterWithLevel) (ιp : MTT.Qbar →+* ℂ_[p])
(L : SeededHorizontalPrimeDataV2 p ιp f η B)
(Θ : SeededFiniteThetaData L)
(hnorm : Θ.SatisfiesNormRelations)
(hunit : Θ.HasUnitEulerFactors) :
∃ μ : SeededNormalizedThetaMeasure L, μ.characters = Θ.characters := by sorry
end HorizontalPadicLSource
Kriz--Nordentoft, https://arxiv.org/pdf/2310.20678, Corollary 5.2 and Definition 5.3.