Iterating prime-power propagation to Corollary 5.17
OpenHorizontalPadicL.primePowerPropagation_iteratedirichlet-charactersnumber-theoryp-adic-l-functions
Elementary iteration over the distinct odd prime-power factors of d/2. At every intermediate stage choose one nonzero twist, excluding N, d and the current seed conductor using B. Retain the quantitative family at the last stage. Coprime products preserve parity and multiply orders and conductors; cancellation bounds multiplicity. Fixed conductor rescaling preserves the logarithmic lower bound. This node contains no horizontal-measure theory.
Preamble
import Definitions.Def_KN_PrimePowerPropagation set_option autoImplicit false noncomputable section open scoped BigOperators
Formal statement
namespace HorizontalPadicL
/-- Elementary iteration over the distinct odd prime-power factors of d/2.
At every intermediate stage choose one nonzero twist, excluding N, d and the
current seed conductor using B. Retain the quantitative family at the last
stage. Coprime products preserve parity and multiply orders and conductors;
cancellation bounds multiplicity. Fixed conductor rescaling preserves the
logarithmic lower bound. This node contains no horizontal-measure theory. -/
theorem primePowerPropagation_iterate
{N k : ℕ} (hN : 0 < N) (hk : 2 ≤ k) (heven : Even k)
(ι : MTT.Qbar →+* ℂ) (f : MTT.Eigenform N k ι)
(hpropagation : HasPrimePowerPropagation ι f)
(harithmetic : PrimitiveProductArithmetic)
(d : ℕ) (hcase1 : d % 4 = 2 ∧ 6 ≤ d)
(η : DirichletCharacterWithLevel)
(hηprim : η.2.IsPrimitive) (hηorder : orderOf η.2 = 2)
(hηeven : η.2 (-1) = 1)
(hηcoprime : Nat.Coprime (N * d) η.2.conductor)
(hηnonzero : @MTT.criticalLValue ι f.form
η.1.1 ⟨Nat.ne_of_gt η.1.2⟩ η.2 (k / 2 - 1) ≠ 0) :
∃ α : ℝ, 0 < α ∧
HasLogPowerLowerBound (eigenformNonvanishingCount ι f d) α := 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.