Orderly congruences bound local p-power exponents
ProvedHorizontalPadicL.SeededHorizontalPrimeSystemV2.orderExponent_le_exponentdirichlet-charactersnumber-theoryp-adic-l-functions
Congruence modulo p^m implies that the maximal local p-power quotient has exponent at least m.
Preamble
import Definitions.Def_KN_PrimePowerPropagation set_option autoImplicit false noncomputable section open scoped BigOperators
Formal statement
namespace HorizontalPadicL
/-- Congruence modulo p^m implies that the maximal local p-power quotient
has exponent at least m. -/
theorem SeededHorizontalPrimeSystemV2.orderExponent_le_exponent
{N k p B : ℕ} {ι : MTT.Qbar →+* ℂ} [Fact p.Prime]
{ιp : MTT.Qbar →+* ℂ_[p]} {f : MTT.Eigenform N k ι}
{η : DirichletCharacterWithLevel}
(L : SeededHorizontalPrimeSystemV2 p ιp f η B) :
∀ n, L.orderExponent ≤ L.exponent n := 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.