# Zulip Chat Archive

## Stream: maths

### Topic: Haar Measure

#### 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 $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 (Jun 18 2020 at 20:06):

(deleted)

#### 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

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

#### 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 $\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 (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.

#### David Wärn (Jun 18 2020 at 21:07):

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

#### Floris van Doorn (Jun 18 2020 at 22:19):

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

#### Jalex Stark (Jun 18 2020 at 22:28):

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

#### Jalex Stark (Jun 18 2020 at 22:29):

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 (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

#### Sebastien Gouezel (Jun 19 2020 at 07:30):

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.

Last updated: May 06 2021 at 17:38 UTC