mathlib

1246edae - feat(analysis/convolution): prove associativity under more convenient assumptions (#16706)

feat(analysis/convolution): prove associativity under more convenient assumptions (#16706) * Prove `convolution_assoc` which has as hypotheses things that are a lot more natural to check. The old version (that has a bit weaker assumptions) is renamed to `convolution_assoc'` * Generalize lemmas about double integrals to the case where we have 2 measures * Consistently use the `is_add_right_invariant` for groups that are not assumed to be abelian (previously I was inconsistent with this for lemmas that only use that multiplication is quasi measure preserving - which follows from either left- or right invariance). * I'm happy to change the definition of `convolution` so that it always plays well with left-invariant measures (instead of the current definition that plays well with right-invariant measures) in a follow-up PR.