Zulip Chat Archive

Stream: maths

Topic: paper about Haar measure


view this post on Zulip 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.

view this post on Zulip 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 Rn\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.

view this post on Zulip 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).

view this post on Zulip 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:

view this post on Zulip 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".

view this post on Zulip Johan Commelin (Feb 16 2021 at 20:25):

which is defined for function that map

"functions"

view this post on Zulip 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?

view this post on Zulip 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{fn(x)}nf(x\ ∶= \sup\{f_n(x)\}_n

view this post on Zulip Johan Commelin (Feb 16 2021 at 20:29):

the integral of a integrable function

"an"

view this post on Zulip 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{fn(x)}nf(x\ ∶= \sup\{f_n(x)\}_n

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

view this post on Zulip Ruben Van de Velde (Feb 16 2021 at 20:37):

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

"into E"?

view this post on Zulip Johan Commelin (Feb 16 2021 at 20:48):

This might not be true right translates

missing "for"?

view this post on Zulip Johan Commelin (Feb 16 2021 at 20:51):

formallize

view this post on Zulip 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"?

view this post on Zulip Johan Commelin (Feb 16 2021 at 21:04):

Cool paper! :thumbs_up: :octopus:

view this post on Zulip Ruben Van de Velde (Feb 16 2021 at 21:16):

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

drop the "a"

view this post on Zulip 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."

view this post on Zulip 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

view this post on Zulip 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 :-/

view this post on Zulip Ruben Van de Velde (Feb 16 2021 at 21:25):

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

view this post on Zulip Kevin Buzzard (Feb 16 2021 at 21:25):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Feb 16 2021 at 21:27):

That stuff at the very end is really neat!

view this post on Zulip Ruben Van de Velde (Feb 16 2021 at 21:28):

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

view this post on Zulip Kevin Buzzard (Feb 16 2021 at 21:29):

in our toolkit

view this post on Zulip 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"?

view this post on Zulip Ruben Van de Velde (Feb 16 2021 at 21:35):

And thanks for sharing, I enjoyed it :)

view this post on Zulip Ruben Van de Velde (Feb 16 2021 at 21:38):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Feb 17 2021 at 01:18):

we expanded the library with products measures

s/products/product/

view this post on Zulip 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. :-)

view this post on Zulip 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.

view this post on Zulip 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