Commit 2026-09-01 11:46 e076e1ca

View on Github →

feat(Integral/Lebesque/Add): add lintegral_lintegral_mul_le (#43283) This PR add the theorem lintegral_lintegral_mul_le, the inequality version of lintegral_lintegral_mul.

Estimated changes

Modified Mathlib/MeasureTheory/Integral/Lebesgue/Add.lean

added theorem MeasureTheory.lintegral_lintegral_mul_le

Modified Mathlib/MeasureTheory/Measure/Prod.lean

modified theorem MeasureTheory.lintegral_prod_le