feat(MagicFunction): shared integrable majorants for contour integrands

[cameronfreer]

The six contour-integrand integrability proofs now use shared bounds for the cusp segments, compact top edges, and vertical tail. This fills the six Φⱼ_integrableOn placeholders and removes repeated estimates from I1.lean–I6.lean.

Stack and merge order

• Depends on feat: improving bounds and restating things in the language of radial Schwartz functions #460; this branch includes its current head. Merge feat: improving bounds and restating things in the language of radial Schwartz functions #460, then refresh this branch from main before merging feat(MagicFunction): shared integrable majorants for contour integrands #463.
• feat(MagicFunction): joint integrability and Fubini for the contour integrals Iⱼ #464 uses the bounds and phase identities here for Fubini. fix(MagicFunction): remove the invalid norm_φ₀_le proof path #468 combines this API with feat(MagicFunction): factorwise estimates for φ₀, φ₂', and φ₄' #304 to retire PolyFourierCoeffBound.norm_φ₀_le.
• feat(MagicFunction): uniform quantitative contour bounds #476 builds on this stack to prove uniform quantitative bounds for all six scalar contour integrals. Its own diff no longer refactors RealDecay.lean or feat: improving bounds and restating things in the language of radial Schwartz functions #460's Decay.lean.
• Supersedes the Integrability.lean portion of feat(Integrability): add Φⱼ integrability proofs #261.

While #460 is unmerged, review the changes relative to its bounding branch; the GitHub diff against main also contains #460.

Changes

• Majorants.lean centralizes the φ₀'' norm estimate, its ray specializations, two integrability lemmas, and the phase identities relating Φ₁, Φ₃, and Φ₅.
• Integrability.lean proves integrability by contour type. I1.lean–I6.lean use the shared estimates directly.
• All six integral comparisons use setIntegral_mono_of_nonneg, eliminating the duplicated nonintegrable-case arguments.
• Removes the six unused whole-real-line decay'₀/decay' placeholders from I2.lean, I4.lean, and I6.lean, together with their empty and commented scaffolding. The nonnegative-input decay goals live in feat: improving bounds and restating things in the language of radial Schwartz functions #460's Schwartz.lean.

The earlier review suggestions from @CBirkbeck and @seewoo5 are incorporated, including removal of the unused specializations and four Bound_integrableOn aliases.

Verification

Full lake build and lake exe mk_all --check --module pass on the combined #460/#463 stack. No new sorry declarations. Φ₂_integrableOn and Φ₄_integrableOn are axiom-clean; the other four still inherit the pre-existing sorry in PolyFourierCoeffBound.norm_φ₀_le, addressed separately by #468.

[seewoo5]

(⚠️ These review are written by Claude)

---

Pulled the branch and reviewed locally. Everything in the PR description checks out:

• Full lake build is clean (3546 jobs); Majorants.lean itself emits zero warnings; project sorry count drops 72 → 66.
• #print axioms confirms the verification claims: Φ₂/Φ₄_integrableOn are sorry-free, and Φ₁/Φ₃/Φ₅/Φ₆_integrableOn depend only on the pre-existing sorryAx from PolyFourierCoeffBound.norm_φ₀_le, untouched here. No new axioms.
• Cross-checked the stacked branches (#464–#468): the inline findings below are all stack-safe (no downstream uses of the flagged declarations), while #464's Fourier/Fubini.lean genuinely consumes norm_φ₀''_I_mul_le, norm_φ₀''_neg_inv_I_mul_le, cexp_pi_I_mul_I, and both phase identities — so the shared-infrastructure design pays off downstream.

Inline comments below. I applied all of them (plus the norm_cexp_pi_I_mul inlining already raised) on top of this branch and the build stays green, net −21 lines.

[seewoo5]

⚠️ Again, these reviews are written by Claude. I explicitly asked to suggest golf/clean-up, based on /mathlib-quality:clean-up skill.

---

Golf/cleanup pass, complementing the earlier correctness review. Every suggestion below is compile-verified twice: first individually against this branch, then all of them applied together (along with the deletions from the earlier review) — full lake build green, no new warnings, all lines ≤ 100 chars. Net effect of the combined set: Majorants.lean 279 → 199 lines (−80), Integrability.lean 95 → 86 (−9), with no statement changes anywhere, so I1–I6 and the stacked PRs (#464, #468) are unaffected.

A few notes that span multiple suggestions:

• The norm_Φ₁_le/norm_Φ₃_le suggestions stop using the private norm_cexp_pi_I_mul, so together with the earlier thread on it, that wrapper ends up with zero callers — deletable.
• neg_one_div_I_mul becomes dead once im_neg_one_div_I_mul is proved directly; those two suggestions should be applied together.
• Recurring wins worth knowing about: Exists.imp absorbs the obtain/refine-existential boilerplate in five lemmas; the phase-identity twins need no I² = −1 at all (the exponent split is a pure ring identity); and hne in im_neg_one_div_add_I was never used (complex division is total).
• Cosmetic, not suggested inline: Φ₂/Φ₄_integrableOn signatures also fit on one line, and mathlib style would prefer 0 ≤ r over r ≥ 0 in the six integrability signatures — but those signatures pre-date this PR.
• Side note for a follow-up, not this PR: with Φ₆_eq_I₆_g + Φ₆_integrableOn in place, I6.lean's header TODO "Integrability of g" is one IntegrableOn.congr_fun away.

[cameronfreer]

@CBirkbeck @seewoo5 Thanks for these reviews. Not sure why there were so many silly issues this time. I think I've addressed all of them.

[seewoo5]

Thanks!

[thefundamentaltheor3m]

Let's merge #460 first and then update this one on top of that. (I'm "requesting changes" so that we don't accidentally merge this one first - and changes will be required once #460 is merged anyway.)

[thefundamentaltheor3m]

@cameronfreer can you please mark resolved conversations as resolved? Thank you