## Stream: maths

### Topic: paper about Haar measure

#### Floris van Doorn (Feb 16 2021 at 18:52):

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 (Feb 16 2021 at 20:00):

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 (Feb 16 2021 at 20:16):

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 (Feb 16 2021 at 20:20):

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

#### Bryan Gin-ge Chen (Feb 16 2021 at 20:24):

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

#### Johan Commelin (Feb 16 2021 at 20:25):

which is defined for function that map

"functions"

#### Ruben Van de Velde (Feb 16 2021 at 20:25):

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 (Feb 16 2021 at 20:28):

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 (Feb 16 2021 at 20:29):

the integral of a integrable function

"an"

#### Johan Commelin (Feb 16 2021 at 20:36):

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 (Feb 16 2021 at 20:37):

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

"into E"?

#### Johan Commelin (Feb 16 2021 at 20:48):

This might not be true right translates

missing "for"?

formallize

#### Johan Commelin (Feb 16 2021 at 20:53):

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

"only integrates some"?

#### Johan Commelin (Feb 16 2021 at 21:04):

Cool paper! :thumbs_up: :octopus:

#### Ruben Van de Velde (Feb 16 2021 at 21:16):

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

drop the "a"

#### Kevin Buzzard (Feb 16 2021 at 21:19):

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 (Feb 16 2021 at 21:23):

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 (Feb 16 2021 at 21:24):

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 (Feb 16 2021 at 21:25):

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

#### Kevin Buzzard (Feb 16 2021 at 21:25):

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

#### Kevin Buzzard (Feb 16 2021 at 21:27):

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 (Feb 16 2021 at 21:27):

That stuff at the very end is really neat!

#### Ruben Van de Velde (Feb 16 2021 at 21:28):

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

in our toolkit

#### Ruben Van de Velde (Feb 16 2021 at 21:31):

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 (Feb 16 2021 at 21:35):

And thanks for sharing, I enjoyed it :)

#### Ruben Van de Velde (Feb 16 2021 at 21:38):

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

#### Floris van Doorn (Feb 16 2021 at 22:00):

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 (Feb 16 2021 at 22:06):

@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 (Feb 16 2021 at 23:27):

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 (Feb 17 2021 at 01:18):

we expanded the library with products measures

s/products/product/

#### Scott Morrison (Feb 17 2021 at 01:22):

@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 (Feb 17 2021 at 06:48):

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 (Feb 17 2021 at 06:49):

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!

Last updated: May 11 2021 at 16:22 UTC