The seeded construction supplies prime-power propagation
OpenHorizontalPadicL.seededHorizontalConstruction_primePowerPropagationdirichlet-charactersnumber-theoryp-adic-l-functions
Select the measure provided by the construction and apply the single-measure propagation theorem. No additional modular-form or density hypothesis is added.
Preamble
import Definitions.Def_KN_PrimePowerPropagation set_option autoImplicit false
Formal statement
namespace HorizontalPadicL
/-- Select the measure provided by the construction and apply the single-measure
propagation theorem. No additional modular-form or density hypothesis is added. -/
theorem seededHorizontalConstruction_primePowerPropagation
{N k : ℕ} (ι : MTT.Qbar →+* ℂ) (f : MTT.Eigenform N k ι)
(hconstruction : HasSeededHorizontalPadicLConstructionV3 ι f) :
HasPrimePowerPropagation ι f := by
sorry
end HorizontalPadicLSource
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.