feat(MeasureTheory/Integral/IntervalIntegral/Fubini): Fubini swap for two iterated interval integrals

[yanghangAI]

Summary

Adds MeasureTheory.intervalIntegral_swap_continuous: Fubini's theorem for two iterated intervalIntegrals on ℝ under joint continuity of the integrand.

lemma intervalIntegral_swap_continuous
    {f : ℝ → ℝ → ℝ} (hf : Continuous (Function.uncurry f)) (a b c d : ℝ) :
    (∫ y in c..d, ∫ x in a..b, f x y) = (∫ x in a..b, ∫ y in c..d, f x y)

Motivation

Mathlib already provides:

• MeasureTheory.integral_integral_swap — swaps two full integrals under product integrability
• MeasureTheory.intervalIntegral_integral_swap — swaps one interval integral with one full integral

Neither directly swaps two iterated interval integrals, which is a common idiom when reducing two-dimensional integrals to iterated one-dimensional ones (for example when reducing a double integral over a rectangle to iterated 1D integrals in calculus proofs). This PR fills that gap.

Proof

The proof handles all four orientation combinations (a ≤ b vs b ≤ a, c ≤ d vs d ≤ c). It reduces to the ordered case via intervalIntegral.integral_symm / intervalIntegral.integral_neg, then converts both interval integrals to a single setIntegral over Set.Icc a b ×ˢ Set.Icc c d via setIntegral_prod and setIntegral_prod_swap. Integrability on the compact product rectangle comes from ContinuousOn.integrableOn_compact.

AI assistance disclosure

This PR was prepared with help from Claude Code (Anthropic's Claude Opus 4.6). Specifically, Claude Code:

• drafted the initial proof structure and the orientation case split;
• located the relevant Mathlib lemmas (setIntegral_prod, setIntegral_prod_swap, ContinuousOn.integrableOn_compact, Ioc_ae_eq_Icc) and wired them together;
• iterated on compiler errors until the proof built cleanly under lake build, lake exe shake, and lake exe lint-style.

All mathematical content was reviewed by me before committing, and I verified the final version builds cleanly in a fresh Mathlib tree. I am responsible for the correctness and style of this PR and will handle any review feedback myself.

Happy to discuss the workflow with maintainers if there's interest or concern.

Zulip

I posted in `#mathlib4 > general` asking if this was duplicate work — no responses yet, proceeding since it's a small standalone helper. Happy to close if this conflicts with anyone's in-flight branch.

[github-actions]

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

[github-actions]

PR summary b43655dfe2

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ intervalIntegral_intervalIntegral_swap
+ intervalIntegral_intervalIntegral_swap_of_continuousOn

You can run this locally as follows

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh 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).

[wwylele]

Continuous seems too strong. The underlying lemma MeasureTheory.setIntegral_prod only requires integrability. I haven't read the code carefully yet, but this looks longer than I expected given interval integral isn't far away from set integral. Have you tried golfing it a bit?

[CoolRmal]

I guess It is still fine to have a version for continuous functions (but you should useContinuousOninstead of using Continuous), but only as a corollary of a version for integrable functions.

Also I don't think it is worth to add a new file for this lemma. You should put it somewhere in Mathlib.MeasureTheory.Integral.Prod or a file about intervalIntegral.

Note that we also have MeasureTheory.integral_integral_swap_of_hasCompactSupport, which possibly can be used to simplify the proof.