[Merged by Bors] - feat: uniqueness of Haar measure in general locally compact groups

[sgouezel]

We prove that two regular Haar measures in a locally compact group coincide up to scalar multiplication, and the same thing for inner regular Haar measures. This is implemented in a new file MeasureTheory.Measure.Haar.Unique. A few results that used to be in the MeasureTheory.Measure.Haar.Basic are moved to this file (and extended) so several imports have to be changed.

---

• depends on: feat: bound the measure of a set by the integral of a function, from above and from below #8123
• depends on: feat: Urysohn lemma in regular locally compact spaces #8124
• depends on: [Merged by Bors] - feat: new class InnerRegular of measures #8251
• depends on: [Merged by Bors] - feat: more facts on measures in topological groups #8286

Unfortunately, I don't see anything that can be split off the current PR. It's one big file MeasureTheory.Measure.Haar.Unique, plus the necessary adaptations to the other files.

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• feat: bound the measure of a set by the integral of a function, from above and from below #8123
• feat: Urysohn lemma in regular locally compact spaces #8124
• [Merged by Bors] - feat: new class InnerRegular of measures #8251
• [Merged by Bors] - feat: more facts on measures in topological groups #8286
  By Dependent Issues (🤖). Happy coding!

[hrmacbeth]

I have a completely surface-level question, having read the statements but not the proofs: is it possible to use lintegral rather than integral thoughout the Uniqueness file, thus downgrading the imports?

[sgouezel]

That's a good question. I have been careful to put that in a new file to avoid polluting more basic files with advanced imports, and normally the files that import this one should be pretty advanced so it shouldn't make a difference, but still.

The basic thing is integrating continuous functions with compact support, so the integral is naturally real-valued. My guess is that it's probably possible to cook up a version using lintegral instead of integral. I'm not sure it would be mathematically more natural, though. One mathematically subtle point is that I need Fubini for compactly supported functions and non-sigma-finite measures on non-second-countable spaces, which I have only implemented for integral, not lintegral.

[RemyDegenne]

Well that was a big one. But it looks great. Thanks!
bors r+

[mathlib-bors]

Build failed (retrying...):

• Build

[mathlib-bors]

Build failed (retrying...):

• Build

[mathlib-bors]

Build failed:

• Build

[sgouezel]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style
• Check all files imported