Commit 2022-10-23 22:06 1246edae

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.