Theorem MeasureTheory.Measure.lintegral_mconv

Modification history

2025-03-25 10:42
Mathlib/MeasureTheory/Group/Convolution.lean
feat(MeasureTheory): add API to convolution of measures and lintegrals (#23292) …
Added MeasureTheory.Measure.lintegral_mconvView on Github →