Construct the faithful seeded horizontal p-adic L-function at an odd prime

Open

HorizontalPadicL.seededHorizontalPadicLFunction_exists_of_primeSystem_v3

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

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

Given an odd prime p, a positive-density orderly-prime system, integral period data, and a nonzero even seed value, construct a horizontal measure whose faithful character evaluations interpolate the corresponding central critical values and whose trivial evaluation is nonzero.

Preamble

import Definitions.Def_KN_SeededHorizontalPadicLFunctionV3
import Theorems.Thm_MTT_birch_mellin_formula

set_option autoImplicit false

Formal statement

namespace HorizontalPadicL

/-- The faithful one-sign horizontal construction at an odd prime. -/
theorem seededHorizontalPadicLFunction_exists_of_primeSystem_v3
    {N k p B : ℕ} [Fact p.Prime]
    (hN : 0 < N) (hk : 2 ≤ k) (heven : Even k)
    (ι : MTT.Qbar →+* ℂ) (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 : SeededHorizontalPrimeSystemV2 p ιp f η B)
    (hseedNonzero :
      @MTT.criticalLValue ι f.form
        η.1.1 ⟨Nat.ne_of_gt η.1.2⟩ η.2 (k / 2 - 1) ≠ 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