Commit 2025-01-02 12:06 8cef41c8
View on Github →feat(MeasureTheory/Integral/SetIntegral): add the restriction of an integral to the support (#20258)
add MeasureTheory.integral_tsupport showing that an integral is equal to its restriction to the support of the integrated function.
motivation: this will be used in #12290 to reduce the integral to the support and enables an estimate by the measure of tsupport and the sup of the function.