paper about Haar measure

Stream: maths

[Floris van Doorn]

I wrote a paper about the formalization of Haar measure in mathlib: https://arxiv.org/abs/2102.07636

It also discusses the measure theory library more generally, in particular the Bochner integral and Fubini's theorem. I had a hard time finding a proof of Fubini's theorem for the Bochner integral in the literature, so when formalizing I followed the proof in Isabelle, (this was formalized by @Johannes Hölzl, who also couldn't give me a reference in the literature for it). So I decided to also carefully write up a proof for it in the paper.
The paper discusses the existence and the uniqueness of the Haar measure, and some of the gaps/mistakes I found in the paper proofs.

[Sebastien Gouezel]

Very nice!

One comment of the very end of the paper: the concept of integrating away a variable seems very much related to the concept of conditional expectation, which is indeed some kind of a generalized integral. You have two sigma-algebras m < m', a function which is m'-measurable, and then the conditional expectation E(f | m) of an m'-measurable function is an m measurable function "integrating away m' / m", in a precise sense. For m the trivial sigma algebra, then E(f | m) is the constant function equal to the integral of f. In $\R^n$, if m' is the usual sigma-algebra and m is the sigma algebra of sets not depending on some coordinate (i.e., products with univ), then I think one gets your notion.

[Johan Commelin]

Nice work! I'm reading it right now.

Some of these definition of a compact set might look unfamiliar, formulated in terms of filters, using in particular the principal filter P and the neighborhood filter N.

This sentence doesn't seem quite right (grammatically).

[Jasmin Blanchette]

I think it's grammatically right ("using" also works as a proposition) but it's surely improvable. :school_crossing:

[Bryan Gin-ge Chen]

The thing that jumps at me is "these definition", it should probably be "these definitions".

[Johan Commelin]

which is defined for function that map

"functions"

[Ruben Van de Velde]

Before we define products, we need some to know that limits of measurable functions are measurable.

Is that "some" supposed to be there?

[Ruben Van de Velde]

And either I'm learning some new syntax, or there's a closing parenthesis missing in $f(x\ ∶= \sup\{f_n(x)\}_n$

[Johan Commelin]

the integral of a integrable function

"an"

[Johan Commelin]

Ruben Van de Velde said:

And either I'm learning some new syntax, or there's a closing parenthesis missing in $f(x\ ∶= \sup\{f_n(x)\}_n$

Also... just after that is a $g(x$... the $g$ seems out of place.

[Ruben Van de Velde]

We can approximate any measurable function f into a E...

"into E"?

[Johan Commelin]

This might not be true right translates

missing "for"?

[Johan Commelin]

formallize

[Johan Commelin]

which is to define a new kind integral that only some variables in the input of a function

"only integrates some"?

[Johan Commelin]

Cool paper! :thumbs_up: :octopus:

[Ruben Van de Velde]

Lemma 11. Let μ and ν be a left invariant regular measures

drop the "a"

[Kevin Buzzard]

which is formulated in the general setting of a
uniform spaces, which simultaneously generalizes metric spaces and topological groups.

-> "which is formulated in the general setting of uniform spaces, which simultaneously generalize metric spaces and topological groups."

[Ruben Van de Velde]

As a consequence, we get the uniqueness of Haar measure: every left invariant measure is a multiple of Haar measure.

Should be "the Haar measure" twice, I think

[Kevin Buzzard]

I think it's OK without "the". But don't ask me why. Maybe the second one should have a "the"? There isn't one Haar measure :-/

[Ruben Van de Velde]

"calculcational" → "calculational" (of this one I'm pretty sure, at least :))

[Kevin Buzzard]

"Another project would be too explore the" -> "...to explore the"

[Kevin Buzzard]

Let me show my ignorance by suggesting that Pontrjagin duality sounds much harder than things like the rep theory of compact groups and Peter-Weyl. Am I completely wrong here? I thought Pontrjagin duality was a whole bunch of subtle harmonic analysis -- I've never got through it.

[Kevin Buzzard]

That stuff at the very end is really neat!

[Ruben Van de Velde]

"the Haar measure as new tool in our toolbelt": "a new tool"?

[Kevin Buzzard]

in our toolkit

[Ruben Van de Velde]

Johan Commelin said:

which is to define a new kind integral that only some variables in the input of a function

"only integrates some"?

And "kind of integral"?

[Ruben Van de Velde]

And thanks for sharing, I enjoyed it :)

[Ruben Van de Velde]

Oh, and the second axiom for normed spaces has mismatched pipes on ||x|

[Floris van Doorn]

Thanks for all the typos and comments! They are very helpful! I incorporated them in my local version, and will upload a new version to arXiv at some point.

[Floris van Doorn]

@Sebastien Gouezel Yes, I think you're right. I think it even more closely fits with the concept of the Marginal distribution, as @Jeremy Avigad pointed out to me recently.

[Jeremy Avigad]

Yes, that's right -- if I am not confused, the marginal distribution is just the conditional expectation with respect to a certain sigma algebra, namely, the sigma algebra of all subsets of the big product that don't depend on the coordinates that you are integrating out.

[Scott Morrison]

we expanded the library with products measures

s/products/product/

[Scott Morrison]

@Floris van Doorn, very nice! One thing that occurs to me --- given that we have such a nice community PR review process, why don't we show it off a little? When you write in the paper that everything has been incorporated in mathlib, could you give a list of links to the PRs themselves? Maybe no one will ever notice, but I think it's a lovely illustration of how well mathlib works. :-)

[Floris van Doorn]

Kevin Buzzard said:

Let me show my ignorance by suggesting that Pontrjagin duality sounds much harder than things like the rep theory of compact groups and Peter-Weyl. Am I completely wrong here? I thought Pontrjagin duality was a whole bunch of subtle harmonic analysis -- I've never got through it.

I have to admit that I actually don't know, but that was my impression from reading about it on Wikipedia.
I'm now looking through a (random) textbook A Course in Abstract Harmonic Analysis by Gerald B. Folland, and the Pontrjagin duality is proven on page 102, a 15 pages after the definition of the dual group. Peter-Weyl's theorem is proven on page 133, 12 pages into the chapter "analysis on compact groups".
So it seems that both these results are pretty basic. I believe Weyl's integration formula is significantly harder though.

[Floris van Doorn]

Scott Morrison said:

Floris van Doorn, very nice! One thing that occurs to me --- given that we have such a nice community PR review process, why don't we show it off a little? When you write in the paper that everything has been incorporated in mathlib, could you give a list of links to the PRs themselves? Maybe no one will ever notice, but I think it's a lovely illustration of how well mathlib works. :-)

That might be interesting to include, indeed!