Package a faithful theta measure as a seeded horizontal p-adic L-function

Proved

HorizontalPadicL.seededHorizontalPadicLFunction_assemble_v2

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

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

A normalized theta measure with faithful character realization, its expected order and surjectivity properties, interpolation, and nonzero trivial value packages with the original positive-density prime system to give the corrected seeded horizontal p-adic L-function.

Preamble

import Definitions.Def_KN_SeededHorizontalPadicLFunctionV3
import Definitions.Def_KN_SeededThetaConstructionV2

set_option autoImplicit false
noncomputable section

Formal statement

namespace HorizontalPadicL

/-- Package a faithful normalized theta measure together with the original
positive-density prime system. -/
theorem seededHorizontalPadicLFunction_assemble_v2
    {N k p B : ℕ} {ι : MTT.Qbar →+* ℂ} [Fact p.Prime]
    (f : MTT.Eigenform N k ι) (hnew : IsNewEigenform f)
    (η : DirichletCharacterWithLevel) (ιp : MTT.Qbar →+* ℂ_[p])
    (L : SeededHorizontalPrimeSystemV2 p ιp f η B)
    (μ : SeededNormalizedThetaMeasureV2 L.toConstructionData)
    (hcharacters : μ.characters.HasExpectedProperties)
    (hinterp : μ.InterpolatesSeededCriticalValues)
    (htrivial : μ.measure.eval
      (trivialHorizontalCharacterV2 p L.toConstructionData.exponent) ≠ 0) :
    ∃ ν : SeededHorizontalPadicLFunctionV2 (B := B) p ιp f η,
      ν.primes = L ∧ ν.InterpolatesSeededCriticalValuesV3 ∧
      ν.measure.eval (trivialHorizontalCharacterV2 p ν.primes.exponent) ≠ 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