Faithful odd-prime normalized theta measure with interpolation

Open

HorizontalPadicL.seededNormalizedThetaMeasure_exists_with_interpolation_v2

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

dirichlet-charactersmodular-formsnumber-theoryp-adic-l-functions

For odd p, normalization of the faithful modular-symbol theta system gives a plus horizontal measure. The pullback compatibility of its character realization and Birch--Stevens identify every character evaluation with the central critical value of the corresponding primitive twist. The trivial horizontal character recovers the seed value.

Deprecated. Its comparison hypothesis unnecessarily included the meaningless zero-modulus case. Use replacement node 6126209e-14ad-4190-bb0e-135eb470c6c9.

Preamble

import Definitions.Def_KN_SeededThetaConstructionV2
import Theorems.Thm_MTT_birch_mellin_formula

set_option autoImplicit false
noncomputable section

Formal statement

namespace HorizontalPadicL

/-- For odd `p`, normalization of the faithful theta system gives a plus
horizontal measure interpolating every horizontal character. -/
theorem seededNormalizedThetaMeasure_exists_with_interpolation_v2
    {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]) (hpodd : p ≠ 2)
    (L : SeededHorizontalPrimeDataV2 p ιp f η B)
    (characters : SeededHorizontalCharacterRealizationV2 L)
    (hcharacters : characters.HasExpectedProperties)
    (scale : IntegralPeriodScale f ιp P)
    (hcomparison : ∀ s j a m, j ≤ k - 2 →
      ι (MTT.algebraicSymbol P s j a m) * P.omega s =
        signedModularSymbol f.form s j a m) :
    ∃ μ : SeededNormalizedThetaMeasureV2 L,
      μ.characters = characters ∧
      μ.InterpolatesSeededCriticalValues ∧
      (μ.measure.eval (trivialHorizontalCharacterV2 p L.exponent) ≠ 0 ↔
        @MTT.criticalLValue ι f.form
          η.1.1 ⟨Nat.ne_of_gt η.1.2⟩ η.2 (k / 2 - 1) ≠ 0) := by
  sorry

end HorizontalPadicL

Source

Kriz--Nordentoft, Horizontal p-adic L-functions, https://arxiv.org/pdf/2310.20678, Corollary 3.6, Definition 5.3, Corollary 5.4, Theorem 5.9, Corollary 5.10 and Corollary 5.17.

View graph