feat(NumberTheory/ModularForms): mean square bound for q-expansions

[loefflerd]

Show that the sum of the norm squares of the first M q-expansion coefficients of a modular cusp form grows like M ^ k, refining the Hecke bound for a single coefficient already in the library.

Upstreamed from the Mazur-Tate-Teitelbaum project on Prove2Me, see https://prove2.me/theorems/2c6274cd-4b5e-49cd-9daa-d45e670e9fdf.

---

AI use: this code was originally AI-written (by a bot run by Chris Birkbeck, instructed to follow some online notes of Zeev Rudnick). The code has been substantially refactored and cleaned up by me for use in Mathlib.

[github-actions]

PR summary 2266872722

Import changes exceeding 2%

%	File
+4.61%	Mathlib.NumberTheory.ModularForms.Bounds

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.NumberTheory.ModularForms.Bounds	3018	3157	+139 (+4.61%)

Import changes for all files

Files	Import difference
Mathlib.NumberTheory.ModularForms.LFunction	119
Mathlib.NumberTheory.ModularForms.Bounds	139

---

Declarations diff (regex)

+ CuspFormClass.exists_sum_range_norm_sq_qExpansion_coeff_le
+ CuspFormClass.exists_sum_range_norm_sq_qExpansion_coeff_le_of_mem_strictPeriods
+ CuspFormClass.sum_range_norm_sq_qExpansion_coeff_isBigO
+ UpperHalfPlane.fourierCoeffOn_neg_eq_zero
+ UpperHalfPlane.qExpansion_coeff_eq_exp_mul_fourierCoeffOn
+ hasSum_norm_sq_qExpansion_coeff_mul_exp
+ sum_range_norm_sq_qExpansion_coeff_le
+ sum_range_norm_sq_qExpansion_coeff_mul_exp_le

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 2266872).

• +8 new declarations
• −0 removed declarations

+CuspFormClass.exists_sum_range_norm_sq_qExpansion_coeff_le
+CuspFormClass.exists_sum_range_norm_sq_qExpansion_coeff_le_of_mem_strictPeriods
+CuspFormClass.sum_range_norm_sq_qExpansion_coeff_isBigO
+UpperHalfPlane.fourierCoeffOn_neg_eq_zero
+UpperHalfPlane.qExpansion_coeff_eq_exp_mul_fourierCoeffOn
+hasSum_norm_sq_qExpansion_coeff_mul_exp
+sum_range_norm_sq_qExpansion_coeff_le
+sum_range_norm_sq_qExpansion_coeff_mul_exp_le

---

No changes to strong technical debt.
No changes to weak technical debt.

Current commit 2266872722
Reference commit 9939342d31

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[CBirkbeck]

This is Chris experimenting with leaving an AI review on this PR. Please feel free to ignore any bits (or all of it)! The review was generated by Claude Code, run by me against a local checkout of this branch; nothing here is blocking and it's all just offered as material to take or leave.

The suggestions below (labelled 1–7) form one consistent set: applying all of them together gives a file that compiles (checked locally by applying exactly these suggestions to the PR head: the two files and everything downstream of them build, lint-style clean). They also work individually, except that the parts of 1 go together, and 6 only makes sense with 3 and 5.

• 1(a)–(d): keep the Fourier / L² import out of QExpansion.lean by moving qExpansion_coeff_eq_exp_mul_fourierCoeffOn to Bounds.lean (the import adds 139 transitive modules to the 19 files downstream of QExpansion.lean; Bounds.lean has one downstream file).
• 2: delete the private MemLp lemma (a two-call wrapper with one use; it's inlined in 3).
• 3: Parseval as an equality (HasSum over ℕ). The negative-index Fourier coefficients of x ↦ f (x + iy) vanish by Cauchy's theorem for z ^ n * cuspFunction h f z on a circle in the q-disc, reusing your change of variables; the Bessel inequality then becomes a one-line corollary.
• 4: sum_range_norm_sq_qExpansion_coeff_le in 5 lines via gcongr (comment kept).
• 5: the mean-square bound for any strict period h (same proof, golfed, comments kept), with the strictWidthInfty statement as a one-line corollary and an IsBigO form.
• 6: module docstring bullets for 3 and 5.
• 7: the MFDeriv/Basic.lean change isn't needed for this PR (hfhol.continuous.comp (by fun_prop) suffices, and ModularFormClass.continuous is already fun_prop), which would avoid rebuilding the 113 files downstream of it; the attributes look like a nice separate small PR.

Two further thoughts, not left as suggestions:

1. A lemma norm_petersson_self : ‖petersson k f f τ‖ = ‖f τ‖ ^ 2 * τ.im ^ k would remove the rpow juggling from hC here, and would also shorten the existing CuspFormClass.exists_bound.
2. A ContinuousOn.memLp_isCompact sibling of MonotoneOn.memLp_isCompact (IsCompact s → ContinuousOn f s → MemLp f p (μ.restrict s), four lines via MemLp.of_bound) would be the natural home for the MemLp fact used in the Bessel argument, though here the direct two-call composition is just as short.

Sanity checks done on the maths: the statements, exponents and normalisations match Rudnick's Petersson-formula notes (Theorem 1.2 and eq. (1)) and Iwaniec, Topics in classical automorphic forms, Theorem 5.1; the exponent k is sharp (Rankin–Selberg) and the constant exp(4π/h) · B² is the one from the notes.

🤖 Generated with Claude Code

[loefflerd]

@CBirkbeck Your bot made some good suggestions, but I'm not super happy with the new lemma fourierCoeffOn_neg_eq_zero: it should be in the UpperHalfPlane namespace for a start, but besides that, the proof seems a bit long and convoluted, very much "first-draft AI output". I'm sure I could golf it if I had to; but can you ask your bot to golf it a bit first? Please also reinstate the fun_prop in hasSum_norm_sq_qExpansion_coeff_mul_exp since I disagreed with suggestion (7).

[CBirkbeck]

@loefflerd Thanks! Two suggestion comments below, again generated by Claude Code (run by me) and compile-checked against the current head 26f0069, with Bounds.lean, LFunction.lean and lint-style clean:

• fourierCoeffOn_neg_eq_zero moved into the UpperHalfPlane namespace with a shorter, less convoluted proof: instead of redoing the circle-integral change of variables, it applies your qExpansion_coeff_eq_intervalIntegral at index 0 to g = 𝕢 ^ (n + 1) * f, whose constant term vanishes because g → 0 at I∞.
• fun_prop reinstated in hasSum_norm_sq_qExpansion_coeff_mul_exp.

🤖 Generated with Claude Code

[CBirkbeck]

Ok I (human Chris) think this all looks good!