Commit 2025-06-02 07:15 5a2eaa85

View on Github →

feat(Analysis): lconvolution API (#25260) Add aemeasurability, associativity and commutativity theorems for mlconvolution (and lconvolution).

Estimated changes

Modified Mathlib/Analysis/LConvolution.lean

added theorem MeasureTheory.aemeasurable_mlconvolution

modified theorem MeasureTheory.measurable_mlconvolution

added theorem MeasureTheory.mlconvolution_assoc

added theorem MeasureTheory.mlconvolution_assoc₀

added theorem MeasureTheory.mlconvolution_comm