Commit 2025-09-23 12:05 d181a582
View on Github →feat(MeasureTheory/Integral/IntegrableOn): add IntegrableOn.of_inter_support
(#29895)
This lemma helps proving integrability in the presence of extra information about the support of a function (e.g. compactly supported / finitely supported).
From the Carleson project.