The generalized Newman bound (newman_delta') #
Γ_Δ(N) satisfies the hypotheses NewmanData N (Γ_Δ(N)) ε_Δ h_Δ of the generic Newman argument
(NewmanGen.lean); the only new ingredient is the element γ_p (exists_gamma_delta):
if j = v_p(ε_Δ) < ν = v_p(N), then p^{j+1} ∣ N, so p^{j+1} ∤ d² − 1 for some d ∈ Δ (otherwise
p^{j+1} ∣ ε_Δ), while p^j ∣ ε_Δ ∣ d² − 1. With t = d and x t − y N = 1, the matrix
[[x, y], [N, t]] lies in Γ_Δ(N), and t(t − x) ≡ t² − 1 (mod N) gives v_p(t − x) = j (gamma_val).
theorem
CongruenceNormalizers.exists_gamma_delta
{N : ℕ}
{Δ : Subgroup (ZMod N)ˣ}
[NeZero N]
{p : ℕ}
(hp : Nat.Prime p)
(hpN : p ∣ N)
(hj : (epsDelta N Δ).factorization p < N.factorization p)
:
The element γ_p of Γ_Δ(N).
theorem
CongruenceNormalizers.newmanData_delta
(N : ℕ)
[NeZero N]
(Δ : Subgroup (ZMod N)ˣ)
:
NewmanData N (GammaDeltaR N Δ) (epsDelta N Δ) (hDelta N Δ)
Γ_Δ(N) satisfies the hypotheses of the generic Newman argument.
theorem
CongruenceNormalizers.newman_delta'
{N : ℕ}
[NeZero N]
(Δ : Subgroup (ZMod N)ˣ)
{g : Matrix.SpecialLinearGroup (Fin 2) ℝ}
(hg : g ∈ NormG (GammaDeltaR N Δ))
:
IsNewmanFormH N (hDelta N Δ) g
The generalized Newman bound.