Commit 2025-03-25 10:42 100c0cd4

feat(MeasureTheory): add API to convolution of measures and lintegrals (#23292) The main theorem of this PR is "mconv_assoc" which shows that the convolution of measures is associative (under the right assumptions). To prove this we add a theorem "Measure.ext_iff" which allows one to show that two measures are equal by showing their lintegrals are equal on all measurable functions. Obviously when one wants to show two measures are equal one could always start with "ext" to introduce a measurable set and then convert to integrals over indicator functions, however I think this theorem provides a good quality of life improvement for proofs that use this structure (and don't use properties of indicators). In light of "mconv_assoc" making the operator left associative seems reasonable (even though it requires a few minor assumptions). Thus I have change "infix" -> "infixl" We also add a theorem "lintegral_mconv" which shows how to compute the lintegral of a function w.r.t a convolution of measures (in analogy with "lintegral_prod") Finally, unless I am missing something I think the names of the theorems "zero_mconv" and "mconv_zero" should be swapped to follow usually convention.