feat(NumberTheory/ModularForms): Parseval for q-expansions and mean square bound for any period (suggestions for #43558)

[CBirkbeck]

Suggestions on top of leanprover-community#43558 (mean square bound for q-expansions), packaged as a draft PR against the DL_modform_parseval branch so that the diff shows only the proposed changes. Take whatever is useful and ignore the rest.

Changes relative to leanprover-community#43558:

• Parseval equality. hasSum_norm_sq_qExpansion_coeff_mul_exp: ∑' n, ‖a n‖² · exp(-4πny/h) = h⁻¹ ∫₀ʰ ‖f(x+iy)‖² dx as a HasSum over ℕ. The negative-index Fourier coefficients of x ↦ f (x + iy) vanish (fourierCoeffOn_neg_eq_zero), proved by Cauchy's theorem for z ^ n * cuspFunction h f z on a circle in the q-disc, reusing the change of variables of qExpansion_coeff_eq_intervalIntegral. The Bessel inequality sum_range_norm_sq_qExpansion_coeff_mul_exp_le is then a one-line corollary (sum_le_hasSum).
• Any strict period. CuspFormClass.exists_sum_range_norm_sq_qExpansion_coeff_le_of_mem_strictPeriods proves the mean-square bound for the q-expansion with respect to any h > 0 in Γ.strictPeriods (same proof); the original strictWidthInfty statement is a one-line specialisation, and CuspFormClass.sum_range_norm_sq_qExpansion_coeff_isBigO is the IsBigO form.
• Imports. qExpansion_coeff_eq_exp_mul_fourierCoeffOn moves from QExpansion.lean to Bounds.lean (which now has public import Mathlib.Analysis.Fourier.AddCircle), so QExpansion.lean no longer imports the Fourier / L² library. That import added 139 transitive modules to the 19 files downstream of QExpansion.lean; Bounds.lean has a single downstream file (LFunction.lean).
• No change to MFDeriv/Basic.lean. The @[fun_prop] attributes on MDifferentiable.continuous / MDifferentiableOn.continuousOn are not needed for this PR (hfhol.continuous.comp (by fun_prop) does the job, and ModularFormClass.continuous is already fun_prop), which avoids rebuilding the 113 files downstream of that file. They may well be worth adding in a separate PR.
• Golfing of the PR's proofs, keeping all proof comments: sum_range_norm_sq_qExpansion_coeff_le (12 → 5 lines via gcongr), exists_sum_range_norm_sq_qExpansion_coeff_le (the rpow juggling in hC becomes one simpa [field, ← Real.rpow_mul_natCast …], the M = 0 case is positivity), qExpansion_coeff_eq_exp_mul_fourierCoeffOn (push_cast [...] absorbs the rewrite chain), and the private MemLp lemma inlined at its only use.

Checked locally: the two files and all 20 modules downstream of them build, no warnings, lint-style clean.

Possible follow-ups not included here: a norm_petersson_self lemma (‖petersson k f f τ‖ = ‖f τ‖ ^ 2 * τ.im ^ k) would simplify hC and CuspFormClass.exists_bound; a ContinuousOn.memLp_isCompact sibling of MonotoneOn.memLp_isCompact.

---

AI use: prepared by Claude (Claude Code) at the direction of Chris Birkbeck, following an automated review of leanprover-community#43558. All Lean was compile-checked; the mathematical claims (Parseval, sharpness of the exponent) were cross-checked against Iwaniec, Topics in classical automorphic forms, Theorem 5.1, and Rudnick's 2019 lecture notes on Petersson's formula, Theorem 1.2.

🤖 Generated with Claude Code

https://claude.ai/code/session_01A6f2mYh682Cc9g7DbpQZ2k