The Main Lemma, per character

Miyake's Lemma 4.6.8: a cusp form f ∈ S_k(Γ₁(N), χ) whose Fourier coefficients vanish at every index coprime to N is a sum, over the primes p ∣ N, of forms in S_k(Γ₁(N), χ) supported on the multiples of p; each such summand is old. This file assembles the descent witness (Newforms/Descent/Coefficient.lean) and the factor dichotomy (Newforms/CoprimeFilter/Dichotomy.lean) into the inductive step and the induction over the primes.

Main results

• TauCeti.mem_cuspFormsOld_of_forall_coprime_qExpansion_coeff_eq_zero: the per-character Main Lemma — a cusp form in S_k(Γ₁(N), χ) whose coefficients vanish at every index coprime to N lies in the old subspace.
• TauCeti.exists_eq_sum_of_forall_coprime_prod_qExpansion_coeff_eq_zero: the induction over a set of primes that proves it.
• TauCeti.exists_mem_qSupportedOnDvdSubmodule_and_qExpansion_coeff_sub_eq_zero: its inductive step, one prime peeled.

Provenance

Adapted from the AINTLIB LeanModularForms project (Chris Birkbeck, Apache-2.0, https://github.com/CBirkbeck/AINTLIB @ eb9621e7bcb0ce220ad53983ec45d987cb5b9002), projects/LeanModularForms/LeanModularForms/StrongMultiplicityOne/InductiveStep.lean and MainLemma.lean — declarations miyake_4_6_8_inductive_step, miyake_4_6_8_induction and mainLemma_charSpace. The source inducts on the cardinality of the set of remaining primes with the decomposition carried as a list; here the induction is on Finset.card with the pieces produced as a function ℕ → CuspForm, and the dichotomy's second branch is consumed through DirichletCharacter.FactorsThrough.

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_mem_qSupportedOnDvdSubmodule_and_qExpansion_coeff_sub_eq_zero {N p : ℕ} [NeZero N] {k : ℤ} (hp : Nat.Prime p) (hpN : p ∣ N) {L : ℕ} (hL : Squarefree L) (hLN : L.primeFactors ⊆ N.primeFactors) (hpL : p.Coprime L) {χ : (ZMod N)ˣ →* ℂˣ} {χ₀ : (ZMod (N / p))ˣ →* ℂˣ} (hcomp : χ = χ₀.comp (ZMod.unitsMap ⋯)) {f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hf : f ∈ cuspFormCharSpace k χ) (hvan : ∀ (n : ℕ), n.Coprime (p * L) → (PowerSeries.coeff n) (UpperHalfPlane.qExpansion 1 ⇑f) = 0) : ∃ g ∈ qSupportedOnDvdSubmodule N k p, g ∈ cuspFormCharSpace k χ ∧ ∀ (n : ℕ), n.Coprime L → (PowerSeries.coeff n) (UpperHalfPlane.qExpansion 1 ⇑(f - g)) = 0

The inductive step of the Main Lemma (Miyake, Lemma 4.6.8). For f ∈ S_k(Γ₁(N), χ) with χ pulled back from χ₀ modulo N / p, vanishing at every index coprime to p L for a squarefree L coprime to p whose primes divide N, there is f_p ∈ S_k(Γ₁(N), χ) supported on the multiples of p with f − f_p vanishing at every index coprime to L: the level-raise V_p of the descent witness of level N / p.

The induction over the primes

theorem TauCeti.exists_eq_sum_of_forall_coprime_prod_qExpansion_coeff_eq_zero {N : ℕ} [NeZero N] {k : ℤ} {χ : (ZMod N)ˣ →* ℂˣ} {S : Finset ℕ} (hS : S ⊆ N.primeFactors) {f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hf : f ∈ cuspFormCharSpace k χ) (hvan : ∀ (n : ℕ), n.Coprime (S.prod id) → (PowerSeries.coeff n) (UpperHalfPlane.qExpansion 1 ⇑f) = 0) : ∃ (g : ℕ → CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k), f = ∑ p ∈ S, g p ∧ (∀ p ∈ S, g p ∈ qSupportedOnDvdSubmodule N k p) ∧ ∀ p ∈ S, g p ∈ cuspFormCharSpace k χ

The coprime sieve decomposes along the primes (Miyake, Lemma 4.6.8, the induction). For S ⊆ N.primeFactors and f ∈ S_k(Γ₁(N), χ) vanishing at every index coprime to the product of S, f = ∑_{p ∈ S} f_p with each f_p ∈ S_k(Γ₁(N), χ) supported on the multiples of p.

The Main Lemma

theorem TauCeti.mem_cuspFormsOld_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 ∈ cuspFormsOld N k

The Main Lemma, per character (Miyake, Lemma 4.6.8; Diamond–Shurman, Theorem 5.7.1): a cusp form in S_k(Γ₁(N), χ) whose Fourier coefficients vanish at every index coprime to N lies in the old subspace. It is a sum, over the primes p ∣ N, of forms of the same nebentypus supported on the multiples of p, and each of those is old.