feat(analysis/convolution): prove associativity under more convenient assumptions

[fpvandoorn]

• 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.

---

• [x] depends on: #16668
• [x] depends on: #16913

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib#16668~~
• ~~leanprover-community/mathlib#16913~~ By Dependent Issues (🤖). Happy coding!

[ocfnash]

Thanks!

bors merge

[bors[bot]]

Build failed:

• Run tests

[PatrickMassot]

bors merge

[bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests