Construct the normalized seeded theta measure with interpolation

Open

HorizontalPadicL.seededNormalizedThetaMeasure_exists_with_interpolation

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

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

Let f be an even-weight new eigenform and eta a primitive even seed character. Given a density-free orderly-prime datum, a horizontal-character realization, a uniform integral period scale, and the comparison between algebraic and signed classical modular symbols, there exists a normalized horizontal theta measure with the prescribed character realization. The resulting measure interpolates nonvanishing of the central critical values of the primitive twists, and its value at the trivial horizontal character is nonzero exactly when the original eta-twist has nonzero central critical value.

The construction, normalization, and interpolation properties are returned together so that interpolation remains attached to the particular measure built from the modular-symbol theta elements.

Deprecated. It does not connect character evaluation to the quotient maps and omits the odd-prime condition needed by the one-sign measure. Use replacement node dae3a001-625e-43b5-a0b5-55f8c0fd9a21.

Preamble

import Definitions.Def_KN_SeededThetaConstruction
import Theorems.Thm_MTT_birch_mellin_formula

set_option autoImplicit false
noncomputable section

Formal statement

namespace HorizontalPadicL

/-- The modular-symbol theta construction, its normalization by unit Euler
factors, and the Birch--Stevens interpolation calculation produce a particular
horizontal measure with the desired interpolation property.

The existential conclusion retains the provenance of the measure: interpolation
is asserted for the measure constructed from the normalized theta elements, not
for an arbitrary `SeededNormalizedThetaMeasure` having the same character
realization. -/
theorem seededNormalizedThetaMeasure_exists_with_interpolation
    {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)
    (characters : SeededHorizontalCharacterRealization L)
    (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) :
    ∃ μ : SeededNormalizedThetaMeasure 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, Corollary 3.6 and Section 5.1, especially equations (5.2)--(5.9); Birch--Stevens interpolation, https://arxiv.org/pdf/2310.20678

View graph