Prove2Me

Quantitative propagation from a seeded horizontal measure

Open
HorizontalPadicL.SeededHorizontalPadicLFunctionV2.primePower_propagation

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

dirichlet-charactersnumber-theoryp-adic-l-functions

Quantitative prime-power propagation from one faithful seeded horizontal measure. The proof sketch separates Fourier theory, realization and counting.

Preamble
import Definitions.Def_KN_PrimePowerPropagation

set_option autoImplicit false
Formal statement
namespace HorizontalPadicL

/-- Quantitative prime-power propagation from one faithful seeded horizontal
measure. The proof sketch separates Fourier theory, realization and counting. -/
theorem SeededHorizontalPadicLFunctionV2.primePower_propagation
    {N k B p : ℕ} {ι : MTT.Qbar →+* ℂ} [Fact p.Prime]
    {ιp : MTT.Qbar →+* ℂ_[p]} {f : MTT.Eigenform N k ι}
    {η : DirichletCharacterWithLevel}
    (ν : SeededHorizontalPadicLFunctionV2 (B := B) p ιp f η)
    (hpodd : p ≠ 2) (m : ℕ) (hm : 0 < m)
    (hexponent : ν.primes.orderExponent = m)
    (hinterp : ν.InterpolatesSeededCriticalValuesV3)
    (htriv : ν.measure.eval
      (trivialHorizontalCharacterV2 p ν.primes.exponent) ≠ 0) :
    ∃ α : ℝ, 0 < α ∧
      HasLogPowerLowerBound
        (seededPrimePowerNonvanishingCount ι f η p m B) α := by
  sorry

end HorizontalPadicL
Source
Kriz--Nordentoft, Horizontal p-adic L-functions, https://arxiv.org/pdf/2310.20678, Section 2.3.3, Lemma 5.7, Theorem 5.9 and Corollary 5.10.

View graph