Prime degeneracy decomposition in the Atkin--Lehner Main Lemma

The Atkin--Lehner Main Lemma says that a cusp form whose Fourier coefficients vanish at every index coprime to its level is old. For a form of fixed nebentypus, the stronger conclusion used in newform theory is an explicit decomposition

f = ∑ p ∣ N, V_p f_p,

where f_p has level N / p. This file derives that sharp form from the prime-supported decomposition of Newforms/MainLemma.lean and the level-lowering dichotomy: each summand supported on multiples of p is the level-raise of a genuine cusp form at level N / p (or is zero).

Main result

• TauCeti.exists_eq_sum_levelRaise_prime_of_forall_coprime_qExpansion_coeff_eq_zero: the prime-degeneracy form of the Main Lemma in a fixed nebentypus space.

Provenance

The mathematical decomposition is Miyake's Lemma 4.6.8 and the sharp form of the Atkin--Lehner Main Lemma in Diamond--Shurman, Theorem 5.7.1. The proof follows the route in the AINTLIB LeanModularForms project (Chris Birkbeck, Apache-2.0, https://github.com/CBirkbeck/AINTLIB at commit eb9621e7bcb0ce220ad53983ec45d987cb5b9002), combining StrongMultiplicityOne/InductiveStep.lean with the level-lowering dichotomy in Eigenforms/ConductorTheorem.lean. Tau Ceti's existing sieve already supplies the prime-supported summands; only the explicit lower-level witnesses are assembled here.

References

• T. Miyake, Modular forms, Lemma 4.6.8.
• F. Diamond and J. Shurman, A first course in modular forms, Theorem 5.7.1.

theorem TauCeti.exists_eq_sum_levelRaise_prime_of_forall_coprime_qExpansion_coeff_eq_zero {N : ℕ} [NeZero N] {k : ℤ} {χ : (ZMod N)ˣ →* ℂˣ} {f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hf : f ∈ cuspFormCharSpace k χ) (hvan : ∀ (n : ℕ), n.Coprime N → (PowerSeries.coeff n) (UpperHalfPlane.qExpansion 1 ⇑f) = 0) : ∃ (F : (p : ↥N.primeFactors) → CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 (N / ↑p))) k), f = ∑ p : ↥N.primeFactors, CuspForm.levelRaise ↑p ⋯ (F p)

Prime-degeneracy form of the Atkin--Lehner Main Lemma, at fixed nebentypus. If f ∈ S_k(N, χ) has vanishing Fourier coefficient at every index coprime to N, then f is a sum of prime degeneracy images V_p f_p, with f_p a cusp form of level N / p for each prime p ∣ N. In particular, this records the lower-level witnesses hidden by the oldspace-membership conclusion of the Main Lemma.