feat(MagicFunction): joint integrability and Fubini for the contour integrals Iⱼ

[cameronfreer]

Joint integrability of the two-variable integrands and the justified interchanges of integration needed to compute the Fourier transform of each Iⱼ.

Where this sits

Depends on: #463 (integrable majorants for the contour integrands), whose pointwise estimates and phase identities this PR consumes. The branch has been refreshed onto #463, including its #460 prerequisite. Review the Fubini module and its supporting additions relative to #463; the diff against main includes the parent stack. After #463 is merged, merge updated main into this branch; the diff will then reduce to this PR's own changes.

Merge order: #460 → #463 → #464, refreshing from main after parent merges.

Depended on by: nothing yet. This is the Fourier-side sibling of the eigenfunction work; the double-zeroes chain (#465 → #466) is independent of it.

Supersedes: #260, and the joint-integrability half of #261. Those branches had accumulated the same stacked history despite addressing different parts of the argument; this replaces them with one focused module.

What changed relative to #260

• Rebuilt from current main, so it picks up the a/Integrability/ reorganisation instead of the pre-reorg file layout.
• No dependency on any double-zero module. ContourEndpoints.lean and VerticalVanishing.lean are not part of this PR; that material now lives in feat(MagicFunction): estimates for the double-zero contour deformation #466.
• Iⱼ_integrable and a_integrable dropped. Integrability of each Iⱼ over ℝ⁸ belongs with the Schwartz structure (feat: improving bounds and restating things in the language of radial Schwartz functions #460's radial Schwartz maps), not here.
• The analytic estimates are no longer restated: they come from Majorants.lean (feat(MagicFunction): shared integrable majorants for contour integrands #463), which is what makes the class-level refactor below possible.

Contents

New SpherePacking/MagicFunction/a/Fourier/Fubini.lean:

The integrands. I₁_integrand–I₆_integrand : ℝ⁸ × ℝ → ℂ, defined from the canonical Φⱼ.

Joint integrability on the product space, by contour type. Two generic routes replace six bespoke proofs:

• prod_integrable_of_gaussian_majorant — if ‖f (x, t)‖ ≤ exp(-π‖x‖²) · w t with w integrable on the segment, the majorant splits and f is integrable on the product space. This settles the compact top edge (I₂, I₄, w constant) and the vertical tail (I₆, w t = C exp(-2πt)).
• prod_integrable_of_mul_unit_phase — transfer along a continuous unit-modulus phase, which is how Φ₁ and Φ₃ inherit from Φ₅.

The cusp class is the one that genuinely differs: the Gaussian there is scaled, exp(-π t ‖x‖²), and its ℝ⁸-integral is t⁻⁴, blowing up as t → 0⁺. The cusp bound exp(-2π/t) · t² beats it, leaving the bounded exp(-2π/t) · t⁻² (integral_norm_I₅_le, resting on the new exp_neg_div_mul_inv_sq_le).

Order of integration. Iⱼ_eq_integral expresses each Iⱼ as a set integral of its integrand, and Iⱼ_integral_swap justifies interchanging ∫_{ℝ⁸} and ∫_{segment}.

Supporting additions

• IntegralParametrisations.lean: continuous_z₂', continuous_z₄', continuous_z₅', continuous_z₆'.
• RealDecay.lean: exp_neg_div_mul_inv_sq_le (exp(-c/t) · t⁻² ≤ exp(-c) for t ∈ (0,1], c ≥ 2).
• Majorants.lean: its cusp specialisation at c = 2π.

Latest cleanup

integral_norm_I₅_le now uses integral_mono_of_nonneg: the left-hand integrand is a norm, so the comparison needs only the Gaussian majorant's integrability, not a separate integrability proof for the norm.

Verification

Full lake build is clean, no new sorrys.