Haar Measure

Stream: maths

[Floris van Doorn]

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 $G$ that is locally compact and Hausdorff. The notes first define the Haar measure on compact sets of $G$, which I will denote $\mu_1$ here. $\mu_1$ is shown to be monotone ($K_1 \subseteq K_2 \Rightarrow \mu_1(K_1)\le\mu_1(K_2)$) and finitely additive ($\mu_1(K_1\cup K_2)=\mu_1(K_1)+\mu_1(K_2)$ if $K_1$ and $K_2$ are disjoint). So it is shown to be a content.
Now we are extending $\mu_1$ to open sets, by defining for an open set $U$ the function $\mu_2(U)=\sup\{\mu_1(K)\mid K\subseteq U,\ K \text{compact}\}$ and it is shown that $\mu_1(K)=\mu_2(K)$ if $K$ is both compact and open (in the notes both these functions are therefore denoted $\mu$).
Then we are extending $\mu_2$ to all sets, by defining $\mu_3(A)=\inf\{\mu_2(U)\mid A\subseteq U,\ U \text{open}\}$. (Basically) the same argument shows that $\mu_3(U)=\mu_2(U)$ if $U$ is an open subset. However, the notes also claim that $\mu_3(K)=\mu_1(K)$ if $K$ is compact, and I don't see how to prove that.

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

[Jalex Stark]

(deleted)

[Jalex Stark]

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

[Floris van Doorn]

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

[Sebastien Gouezel]

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 $\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 $\mu_1$ which is itself nonzero.

[Floris van Doorn]

@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.

[David Wärn]

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

[Floris van Doorn]

That's true.; I do want that.

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

[Floris van Doorn]

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

[Jalex Stark]

is there a neighborhood of identity with finite $\mu_3$?

[Jalex Stark]

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

[Kevin Buzzard]

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

[Sebastien Gouezel]

David Wärn said:

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

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