Prove2Me

Seeded interpolation at the trivial horizontal character

Proved
HorizontalPadicL.seededNormalizedThetaMeasure_trivial_interpolation

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

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

If the faithful realization sends the trivial horizontal character to the trivial Dirichlet character, the general seeded interpolation property specializes to the original primitive seed character.

Preamble
import Definitions.Def_KN_SeededFiniteThetaCriticalZeroSet

set_option autoImplicit false
noncomputable section
Formal statement
namespace HorizontalPadicL

/-- The general seeded interpolation property specializes at the trivial
horizontal character to the original primitive seed character. -/
theorem seededNormalizedThetaMeasure_trivial_interpolation
    {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}
    (hηprim : η.2.IsPrimitive)
    (characters : SeededHorizontalCharacterRealizationV2 L)
    (hcharacters : characters.HasExpectedProperties)
    (μ : SeededNormalizedThetaMeasureV2 L)
    (hμcharacters : μ.characters = characters)
    (hinterp : μ.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
Formal specialization of the seeded interpolation definition; Kriz--Nordentoft, Corollary 5.4.

View graph