Zulip Chat Archive

Stream: maths

Topic: Haar Measure


view this post on Zulip Floris van Doorn (Jun 18 2020 at 20:02):

I am formalizing the Haar measure in Lean, following these notes. There is one place where the notes are handwaving, and I'm not sure how to fill in the gap (on paper).

So we are given a topological group GG that is locally compact and Hausdorff. The notes first define the Haar measure on compact sets of GG, which I will denote μ1\mu_1 here. μ1\mu_1 is shown to be monotone (K1K2μ1(K1)μ1(K2)K_1 \subseteq K_2 \Rightarrow \mu_1(K_1)\le\mu_1(K_2)) and finitely additive (μ1(K1K2)=μ1(K1)+μ1(K2)\mu_1(K_1\cup K_2)=\mu_1(K_1)+\mu_1(K_2) if K1K_1 and K2K_2 are disjoint). So it is shown to be a content.
Now we are extending μ1\mu_1 to open sets, by defining for an open set UU the function μ2(U)=sup{μ1(K)KU, Kcompact}\mu_2(U)=\sup\{\mu_1(K)\mid K\subseteq U,\ K \text{compact}\} and it is shown that μ1(K)=μ2(K)\mu_1(K)=\mu_2(K) if KK is both compact and open (in the notes both these functions are therefore denoted μ\mu).
Then we are extending μ2\mu_2 to all sets, by defining μ3(A)=inf{μ2(U)AU, Uopen}\mu_3(A)=\inf\{\mu_2(U)\mid A\subseteq U,\ U \text{open}\}. (Basically) the same argument shows that μ3(U)=μ2(U)\mu_3(U)=\mu_2(U) if UU is an open subset. However, the notes also claim that μ3(K)=μ1(K)\mu_3(K)=\mu_1(K) if KK is compact, and I don't see how to prove that.

Translating this question back to just μ1\mu_1 and μ2\mu_2, the question is: "Given a compact set KK and ε>0\varepsilon>0 there is an open set UKU\supseteq K such that μ2(U)μ1(K)+ε\mu_2(U)\le \mu_1(K)+\varepsilon". How do I find this UU?

view this post on Zulip Jalex Stark (Jun 18 2020 at 20:06):

(deleted)

view this post on Zulip Jalex Stark (Jun 18 2020 at 20:29):

maybe if you leave it as a sorry instead of an informal statement, it's more likely that someone will come along and fill it

view this post on Zulip Floris van Doorn (Jun 18 2020 at 20:49):

It's this sorry. Note that I'm only asking for the proof idea. I'm happy to formalize that idea myself.

view this post on Zulip Sebastien Gouezel (Jun 18 2020 at 20:49):

I don't think it is obvious (I am not even sure it is true!) But you don't need that to construct the Haar measure: your μ3\mu_3 is a measure (that's a general property when you start from a content and do what you have done), it is left-invariant as everything is in the construction. And the main point is that it is nonzero, which follows from the fact that it is bounded below by μ1\mu_1 which is itself nonzero.

view this post on Zulip Floris van Doorn (Jun 18 2020 at 20:50):

@Sebastien Gouezel Ok, that makes sense. I was already continuing without that fact, but I wasn't sure if I needed it later. Good to know that I don't need it.

view this post on Zulip David Wärn (Jun 18 2020 at 21:07):

I guess what you want to know is that μ3(K)<\mu_3(K) < \infty for KK compact?

view this post on Zulip Floris van Doorn (Jun 18 2020 at 22:19):

That's true.; I do want that.

There is also a fixed compact set K0K_0 such that μ1(K0)=1\mu_1(K_0)=1, and it would be nice (though not necessary) to have μ3(K0)=1\mu_3(K_0)=1.

view this post on Zulip Floris van Doorn (Jun 18 2020 at 22:20):

I will try to find other sources which might have proven (or worked around) this fact in more detail.

view this post on Zulip Jalex Stark (Jun 18 2020 at 22:28):

is there a neighborhood of identity with finite μ3 \mu_3 ?

view this post on Zulip Jalex Stark (Jun 18 2020 at 22:29):

if so, you can translate that to get a μ3 \mu_3 -finite neighborhood of every point. Then K is covered by finitely many of those, to it's μ3 \mu_3 -finite

view this post on Zulip Kevin Buzzard (Jun 18 2020 at 23:24):

I thought P J Higgins' book on topological groups did a very thorough job on Haar measure but I looked in it this evening to see if I could find your result and found that he sets it all up via Haar integrals

view this post on Zulip Sebastien Gouezel (Jun 19 2020 at 07:30):

David Wärn said:

I guess what you want to know is that μ3(K)<\mu_3(K) < \infty for KK compact?

This is easy: fix a nonempty open set UU with compact closure KK (it exists since the space is locally compact). Then μ3(U)μ1(K)\mu_3(U) \leq \mu_1(K) by monotonicity of μ1\mu_1, hence μ3(U)\mu_3(U) is finite. Then, any compact set LL is included in a finite number of left translates of UU, and has therefore finite μ3\mu_3 measure.


Last updated: May 06 2021 at 17:38 UTC