University of Pittsburgh,
USAfpvdoorn@gmail.comhttps://orcid.org/0000-0003-2899-8565The author is
supported by the Sloan Foundation (grant G-2018-10067) Floris van Doorn
<ccs2012> <concept> <concept_id>10003752.10003790.10011740</concept_id>
<concept_desc>Theory of computation Type theory</concept_desc>
<concept_significance>500</concept_significance> </concept> <concept>
<concept_id>10002950.10003714</concept_id> <concept_desc>Mathematics of
computing Mathematical analysis</concept_desc>
<concept_significance>500</concept_significance> </concept> </ccs2012>
[500]Theory of computation Type theory [500]Mathematics of computing
Mathematical analysis

###### Acknowledgements.

I want to thank Jeremy Avigad and Tom Hales for proofreading this paper.John
Q. Open and Joan R. Access 2 42nd Conference on Very Important Topics (CVIT
2016) CVIT 2016 CVIT 2016 December 24–27, 2016 Little Whinging, United Kingdom
42 23

# Formalized Haar Measure

Floris van Doorn

###### Abstract

We describe the formalization of the existence and uniqueness of Haar measure
in the Lean theorem prover. The Haar measure is an invariant regular measure
on locally compact groups, and it has not been formalized in a proof assistant
before. We will also discuss the measure theory library in Lean’s mathematical
library mathlib, and discuss the construction of product measures and the
proof of Fubini’s theorem for the Bochner integral.

###### keywords:

Haar measure, measure theory, Lean, interactive theorem proving, formalized
mathematics

###### category:

##  1 Introduction

Measure theory is an important part of mathematics, providing a rigorous basis
for integration and probability theory. The main object of study in this part
is the concept of a measure, that assigns a size to the measurable subsets of
the space in question. The most widely used measure is the Lebesgue measure
$\lambda$ on $\mathbb{R}$ (or $\mathbb{R}^{n}$) with the property that
$\lambda([a,b])=b-a$. The Lebesgue measure is _translation invariant_ ,
meaning that translating a measurable set does not change its measure.

An important generalization of the Lebesgue measure is the Haar measure, which
provides a measure on locally compact groups. This measure is also invariant
under translations, i.e. applying the group operation. For non-abelian groups
we have to distinguish between left and right Haar measures, which are
invariant when applying the group operation on the left and right,
respectively. A Haar measure is essentially unique, which means that any
invariant measure is a constant multiple of a chosen Haar measure. The Haar
measure is vital in various areas of mathematics, including harmonic analysis,
representation theory, probability theory and ergodic theory.

In this paper we describe the formal definition of the Haar measure in the
Lean theorem prover [6], and prove its uniqueness. We build on top of the Lean
mathematical library mathlib [5]. We heavily use the library for measure
theory in mathlib, improving it in the process. As part of this formalization
we expanded the library with products measures and Fubini’s theorem, along
with many other contributions to existing libraries. The results in this paper
have been fully incorporated into mathlib.

Many proof assistants have a library of measure theory and integration,
including Isabelle [17, 13], HOL/HOL4 [14, 2, 16], HOL Light [12], Mizar [8]
and PVS [15]. Most of these libraries focus on the Lebesgue measure and the
Lebesgue integral, and on applications to probability theory or analysis in
Euclidean spaces.

The Isabelle/HOL library has an especially good development of measure theory,
including product measures and the Bochner integral [1]. The Lean library also
has these concepts, and the development of them was heavily inspired by the
Isabelle/HOL library. However, to my knowledge, the Haar measure has not been
formalized in any proof assistant other than Lean.

In this paper we will discuss the measure theory library in Lean (in Section
3), which was already in place before this formalization started, and was
developed by Johannes Hölzl, Mario Carneiro, Zhouhang Zhou and Yury
Kudryashov, among others. The other sections describe contributions that are
new as of this formalization: product measures (in Section 4), the definition
of the Haar measure (in Section 5), and the uniqueness of the Haar measure (in
Section 6).

We will link to specific results in mathlib using the icon
${}^{\text{\faExternalLink}}$. To ensure that these links will work while
mathlib is updated, we link to the version of mathlib as of writing this
paper. Readers of this paper are also encouraged to use the search function of
the mathlib documentation pages ${}^{\text{\faExternalLink}}$ but we do not
link to specific pages of the documentation, as these links are prone to break
as the library evolves.

We used different sources for this formalization. We started out using the
notes by Jonathan Gleason [9] that gave a construction of the Haar measure in
detail. However, one of the main claims in that paper was incorrect, as
described in Section 5. We then used the books by Halmos and Cohn [11, 3] to
fill in various details. For product measures we followed Cohn [3]. However,
we could not find a good source for the proof of Fubini’s theorem for the
Bochner integral, other than the formalization in Isabelle. For this reason,
we will provide detailed proofs of that result in Section 4. For the
uniqueness of Haar measure we followed Halmos [11]. While we define the Haar
measure for any locally compact group, we prove the uniqueness only for
second-countable locally compact groups. The reason is that Halmos gives a
uniqueness proof using measurable groups, and only second-countable
topological groups form measurable groups. In the proof of a key theorem of
Halmos there was a gap, which we fixed in the formalization by changing the
statement of that theorem.

##  2 Preliminaries

###  2.1 Lean and mathlib

Lean [6] is a dependently typed proof assistant with a strong metaprogramming
framework [7]. It has a large community-driven mathematical library, called
mathlib. We use results from various areas in this library, including
topology, analysis and algebra. In particular the existing library for
topological groups was very helpful for this formalization. The fact that Lean
provides a very expressive type theory was convenient in the definition of the
Bochner integral, as we will discuss in Section 3.

mathlib uses _type-classes_ [19, 18] to organize the mathematical structures
associated to various types, using the partially bundled approach. For
example, when G is a type, the statement [group G] states that G has the
structure of a group, and [topological_space G] states that G has the
structure of a topological space. The square brackets mean that the argument
will be implicitly inserted in definitions and theorems using type-class
inference. Some type-classes are _mixins_ , and take other type-classes as
arguments. For example, the class topological_group takes as arguments classes
for group and topological_space (which are implicit). This means that we need
to write [group G] [topological_space G] [topological_group G] to state that G
is a topological group. Similarly, predicates on topological spaces — such as
t2_space, locally_compact_space or compact_space — take the topological space
structure as argument. This design decision makes it somewhat verbose to get
the right structure on a type, but has the advantage that these components can
be freely mixed as needed.

Lean distinguishes groups written multiplicatively (group) from groups written
additively (add_group). This is convenient since it automatically establishes
multiplicative notation (1 * x⁻¹) or additive notation (0 + -x or 0 - x) when
declaring a group structure. Also, most theorems exist for both versions; the
property x * y = y * x is called mul_comm and the property x + y = y + x is
add_comm. To avoid code duplication, there is an attribute @[to_additive]
that, when applied to a definition or theorem for multiplicative groups,
automatically generates the corresponding declaration for additive groups by
replacing all multiplicative notions with the corresponding additive ones.

Some code snippets in this paper have been edited slightly for the sake of
readability.

###  2.2 Mathematics in mathlib

The notation for the image of a set A : set X under a function f : X → Y is f '' A = {y : Y | ∃ x ∈ A, f x = y} and the preimage of B : set Y is f ⁻¹' B = {x : X | f x ∈ B}. The notation λ x, f x is used for the function $x\mapsto f(x)$. We write (x : X) for the element x with its type X given explicitly. This can also be used to _coerce_ x to the type X.

mathlib has a large topology library, where many concepts are defined in terms
of filters. The following code snippet contains some notions in topology used
in this paper.

⬇

class t2_space (X : Type*) [topological_space X] : Prop :=

(t2 : ∀ x y, x ≠ y → ∃ U V : set X, is_open U ∧ is_open V ∧

x ∈ U ∧ y ∈ V ∧ U ∩ V = ∅)

def is_compact {X : Type*} [topological_space X] (K : set X) :=

∀ ⦃f : filter X⦄ [ne_bot f], f ≤ 𝓟 K → ∃ x ∈ K, cluster_pt x f

class locally_compact_space (X : Type*) [topological_space X] : Prop :=

(local_compact_nhds : ∀ (x : X) (U ∈ 𝓝 x), ∃ K ∈ 𝓝 x, K ⊆ U ∧

is_compact K)

class second_countable_topology : Prop :=

(is_open_generated_countable : ∃ C : set (set X), countable C ∧

t = generate_from C)

class complete_space (X : Type*) [uniform_space X] : Prop :=

(complete : ∀ {f : filter α}, cauchy f → ∃ x, f ≤ 𝓝 x)

class topological_group (G : Type*) [topological_space G] [group G] :=

(continuous_mul : continuous (λ p : G × G, p.1 * p.2))

(continuous_inv : continuous (inv : G → G))

Some of these definition of a compact set might look unfamiliar, formulated in
terms of filters, using in particular the principal filter 𝓟 and the
neighborhood filter 𝓝. For example, the second definition states that a set K
is _compact_ ${}^{\text{\faExternalLink}}$ if any filter f ≠ ⊥ containing K
has a cluster point x in K, which means that 𝓝 x ⊓ f ≠ ⊥. It is equivalent to
the usual notion of compactness that every open cover of K has a finite
subcover. ${}^{\text{\faExternalLink}}$ A complete space is a space where
every Cauchy sequence converges, ${}^{\text{\faExternalLink}}$ which is
formulated in the general setting of a _uniform spaces_ , which simultaneously
generalizes metric spaces and topological groups. We define a _locally compact
group_ to be a topological group in which the topology is both locally compact
and Hausdorff ($T_{2}$)

Lean’s notion of infinite sums is defined for absolutely convergent series as
the limit of all finite partial sums: ${}^{\text{\faExternalLink}}$

⬇

def has_sum [add_comm_monoid M] [topological_space M]

(f : I → M) (x : M) : Prop :=

tendsto (λ s : finset I, ∑ i in s, f i) at_top (𝓝 x)

If M is Hausdorff, then the sum is unique if it exists, and we denote it by ∑'
i, f i. If the series does not have a sum, it is defined to be 0.

The type ennreal ${}^{\text{\faExternalLink}}$ is the type of nonnegative real
numbers extended by a new element $\infty$, which we will also denote
$[0,\infty]$ in this paper.

A _normed space_ ${}^{\text{\faExternalLink}}$ $X$ is a vector space over a
normed field $F$ equipped with a norm $\|{\cdot}\|:X\to\mathbb{R}$ satisfying

  * •

$(X,d)$ is a metric space, with the distance function given by
$d(x,y)\vcentcolon=\|x-y\|$.

  * •

for $r\in F$ and $x\in X$ we have $\|r\cdot x\|=\|r\|\cdot\|x|$.

In this paper, we will only consider normed spaces over $\mathbb{R}$, which is
a normed field with its norm given by the absolute value. A _Banach space_ is
a complete normed space. In Lean we do not explicitly define Banach spaces,
but instead talk about complete normed spaces.

##  3 Measure Theory in mathlib

In this section we describe the background measure theory library used in this
formalization.

A basic notion in measure theory is a _$\upsigma$ -algebra_ on $X$, which is a
nonempty collection of subsets of $X$ that is closed under complements and
countable unions. In mathlib this is formulated as a type-class, with name
measurable_space: ${}^{\text{\faExternalLink}}$

⬇

class measurable_space (X : Type*) :=

(is_measurable : set X → Prop)

(is_measurable_empty : is_measurable ∅)

(is_measurable_compl : ∀ A, is_measurable A → is_measurable Aᶜ)

(is_measurable_Union : ∀ A : ℕ → set X, (∀ i, is_measurable (A i)) →

is_measurable (⋃ i, A i))

We say that a function is _measurable_ if the preimage of every measurable set
is measurable: ${}^{\text{\faExternalLink}}$

⬇

def measurable [measurable_space X] [measurable_space Y] (f : X → Y) :=

∀ ⦃B : set Y⦄, is_measurable B → is_measurable (f ⁻¹' B)

Note that we use is_measurable for sets and measurable for functions.

In mathlib, measures are defined as special case of outer measures. An outer
measure on $X$ is a monotone function $m:\mathcal{P}(X)\to[0,\infty]$ such
that $m(\emptyset)=0$ and $m$ is countably subadditive:
${}^{\text{\faExternalLink}}$

⬇

structure outer_measure (X : Type*) :=

(measure_of : set X → ennreal)

(empty : measure_of ∅ = 0)

(mono : ∀ {A₁ A₂}, A₁ ⊆ A₂ → measure_of A₁ ≤ measure_of A₂)

(Union_nat : ∀ (A : ℕ → set X),

measure_of (⋃ i, A i) ≤ (∑' i, measure_of (A i)))

A measure on a measurable space is an outer measure with two extra properties:
it is countably additive on measurable sets, and given the value on measurable
sets, the outer measure is the maximal one that is compatible with these
values (which is called trim in the snippet below).
${}^{\text{\faExternalLink}}$

⬇

structure measure (X : Type*) [measurable_space X]

extends outer_measure X :=

(m_Union : ∀ ⦃A : ℕ → set X⦄,

(∀ i, is_measurable (A i)) → pairwise (disjoint on A) →

measure_of (⋃ i, A i) = ∑' i, measure_of (A i))

(trimmed : to_outer_measure.trim = to_outer_measure)

This definition has two very convenient properties:

  1. 1.

We can apply measures to any set, without having to provide a proof that the
set is measurable.

  2. 2.

Two measures are equal when they are equal on measurable sets.
${}^{\text{\faExternalLink}}$

Given a measure $\mu$ on $X$ and a map $f:X\to Y$, we can define the
_pushforward_ $f_{*}\mu$, ${}^{\text{\faExternalLink}}$ which is a measure on
$Y$, defined on measurable sets $A$ by $(f_{*}\mu)(A)=\mu(f^{-1}(A))$.
${}^{\text{\faExternalLink}}$

We proceed to define lower Lebesgue integration $\int^{-}$ for functions
$f:X\to[0,\infty]$, where $X$ is a measurable space. We annotate this integral
with a minus sign to distinguish it from the Bochner integral. This is done
first for _simple functions_ , i.e. functions with finite range with the
property that the preimage of all singletons are measurable. The integral of a
simple function $g$ is simply ${}^{\text{\faExternalLink}}$

$\int^{-}g\,\mathrm{d}\mu=\int^{-}g(x)\,\mathrm{d}\mu(x)=\sum_{y\in
g(X)}\mu(g^{-1}\\{y\\})\cdot y\in[0,\infty].$

If $f:X\to[0,\infty]$ is any function, we can define the _(lower) Lebesgue
integral_ of $f$ to be the supremum of $\int^{-}g\,\mathrm{d}\mu(x)$ for all
simple functions $g$ that satisfy $g\leq f$ (pointwise).
${}^{\text{\faExternalLink}}$ In mathlib we denote the Lebesgue integral of f
by ∫⁻ x, f x ∂μ. We prove the standard properties of the Lebesgue integral for
nonnegative functions, such as the monotone convergence theorem:
${}^{\text{\faExternalLink}}$

⬇

theorem lintegral_supr {f : ℕ → X → ennreal}

(hf : ∀ n, measurable (f n)) (h_mono : monotone f) :

(∫⁻ x, ⨆ n, f n x ∂μ) = (⨆ n, ∫⁻ x, f n x ∂μ)

After defining the Lebesgue integral for nonnegative functions, most books and
formal libraries continue to define the Lebesgue integral for (signed)
functions $f:X\to\mathbb{R}$. This is defined as the difference of the
integrals of the positive and negative parts of $f$. However, this is not very
general: separate definitions are needed for integrals for functions with
codomain $\mathbb{C}$ or $\mathbb{R}^{n}$. Instead, we opt for the more
general definition of the _Bochner integral_ , which is defined for function
that map into any second-countable real Banach space.

If $X$ is a topological space, we equip it with the _Borel_
$\upsigma$-algebra, which is the smallest $\upsigma$-algebra that contains all
open sets (or equivalently, all closed sets). ${}^{\text{\faExternalLink}}$
The fact that $X$ is equipped with the Borel $\upsigma$-algebra is a mixin,
and is specified by providing the arguments [topological_space X]
[measurable_space X] [borel_space X].

Let $X$ be a measurable space and $E$ be a second-countable real Banach space.
We define two quotients on functions from $X$ to $E$.

Let $X\to_{\mu}E$ be the measurable maps $X\to E$ modulo $\mu$-a.e.
equivalence, i.e. modulo the relation

$f=_{\mu}g\Longleftrightarrow\mu(\\{x\mid f(x)\neq
g(x)\\})=0.\leavevmode\nobreak\ \href https://github.com/leanprover-
community/mathlib/blob/2cbaa9cc29bc44812b679810352ed383f35dcf75/src/measure_theory/ae_eq_fun.lean#L93\
$

Note that we are using the fact that Lean is based on dependent type theory
here, since $X\to_{\mu}E$ is a type that depends on $\mu$. Here our
formalization differs from the one in Isabelle, since in Isabelle this type
cannot be formed. Instead, a similar argument is given purely on functions,
without passing to the quotient.

If $f:X\to E$ we say that $f$ is _integrable_ if ${}^{\text{\faExternalLink}}$

  * •

$f$ is $\mu$-a.e. measurable, i.e. there is a measurable function $g:X\to E$
with $f=_{\mu}g$;111Until recently, the definition of “integrable” in mathlib
required $f$ to be measurable. The definition was modified to increase
generality. The motivating reason was that we would regularly take integrals
of a function $f$ with a measure $\mu|_{A}$ defined by $\mu|_{A}(B)=\mu(A\cap
B)$. A function that is (for example) continuous on $A$ is also
$\mu|_{A}$-a.e. measurable, and we usually do not need any information about
the behavior of $f$ outside $A$, so it is not necessary to assume that $f$ is
measurable everywhere. and

  * •

$\int^{-}\|f(x)\|\,\mathrm{d}\mu(x)<\infty.$

The $L^{1}$-space $L^{1}(X,\mu;E)$ is defined as those equivalence classes of
functions in $X\to_{\mu}E$ that are integrable. ${}^{\text{\faExternalLink}}$
$L^{1}(X,\mu;E)$ is a normed space, ${}^{\text{\faExternalLink}}$ with the
norm given by

$\|f\|\vcentcolon=\int^{-}\|f(x)\|\,\mathrm{d}\mu(x).$

We define the Bochner integral first for simple functions, similar to the
definition for the Lebesgue integral. If $g:X\to E$ is a simple function then
its Bochner integral is ${}^{\text{\faExternalLink}}$

$\int g\,\mathrm{d}\mu=\int
g(x)\,\mathrm{d}\mu(x)=\sum_{\begin{subarray}{c}y\in g(X)\text{ s.t.}\\\
\mu(g^{-1}\\{y\\})<\infty\end{subarray}}\mu(g^{-1}\\{y\\})\cdot y\in E.$

The symbol $\cdot$ denotes the scalar multiplication in the Banach space $E$.
Since this definition respects $\mu$-a.e. equivalence, we can also define the
Bochner integral on the simple $L^{1}$ functions.
${}^{\text{\faExternalLink}}$ On the simple $L^{1}$ functions this definition
is continuous ${}^{\text{\faExternalLink}}$ and the simple $L^{1}$ functions
are dense in all $L^{1}$ functions, ${}^{\text{\faExternalLink}}$ and $E$ is
complete, so we can extend the Bochner integral to all $L^{1}$ functions.
${}^{\text{\faExternalLink}}$

Finally, for an arbitrary function $f:X\to E$ we define its Bochner integral
to be $0$ if $f$ is not integrable and the integral of $[f]\in L^{1}(X,\mu;E)$
otherwise. ${}^{\text{\faExternalLink}}$ If we take the integral of a
integrable function $X\to\mathbb{R}_{\geq 0}$, then the two choices agree:
${}^{\text{\faExternalLink}}$

$\int^{-}f\,\mathrm{d}\mu=\int f\,\mathrm{d}\mu.$

However, when $f$ is not integrable, then the equality does not hold: the LHS
is $\infty$, while the RHS is $0$. We then prove useful properties about the
Bochner integral, such as the dominated convergence theorem:
${}^{\text{\faExternalLink}}$

⬇

theorem tendsto_integral_of_dominated_convergence

{F : ℕ → X → E} {f : X → E} (bound : X → ℝ)

(F_measurable : ∀ n, ae_measurable (F n) μ)

(f_measurable : ae_measurable f μ)

(bound_integrable : integrable bound μ)

(h_bound : ∀ n, ∀ᵐ x ∂μ, ∥F n x∥ ≤ bound x)

(h_lim : ∀ᵐ x ∂μ, tendsto (λ n, F n x) at_top (𝓝 (f x))) :

tendsto (λ n, ∫ x, F n x ∂μ) at_top (𝓝 (∫ x, f x ∂μ))

In this statement, ∀ᵐ x ∂μ, P x means that P x holds for μ-almost all x, in other words that μ { x | ¬ P x } = 0, and tendsto (λ n, g n) at_top (𝓝 x) means that g n tends to x as n tends to ∞.

Other results about integration include part 1 ${}^{\text{\faExternalLink}}$
and 2 ${}^{\text{\faExternalLink}}$ of the fundamental theorem of calculus,
but we will not use these results in this paper.

##  4 Products of Measures

To prove that the Haar measure is essentially unique, we need to work with
product measures and iterated integrals. In this section we will define the
product measure and prove Tonelli’s and Fubini’s theorem. (Sometimes both
theorems are called Fubini’s theorem, but in this paper we will distinguish
them.) Tonelli’s theorem characterizes the Lebesgue integral for nonnegative
functions in the product space, and Fubini’s theorem does the same (under
stronger conditions) for the Bochner integral. By symmetry, both theorems also
give sufficient conditions for swapping the order of integration when working
with iterated integrals.

The contents of this section have been formalized before in Isabelle. Product
measures, Tonelli’s theorem and Fubini’s theorem for the Lebesgue integral are
discussed in the paper [13]. Fubini’s theorem for the Bochner integral is
significantly harder to prove, but has also been formalized in Isabelle after
the appearance of that paper. ${}^{\text{\faExternalLink}}$ We could not find
a good source for the proof of Fubini’s theorem for the Bochner integral, so
we read through the proof in the Isabelle formalization for key ideas in
various intermediate lemmas. For this reason, we will provide detailed proofs
of the results in the section.

In this section we will restrict our attention to $\upsigma$-finite measures,
since product measures are much nicer for $\upsigma$-finite measures, and most
of the results do not hold without this condition. We say that a measure $\mu$
on a space $X$ is $\upsigma$-finite if $X$ can be written as a union of
countably many subsets $(A_{i})_{i}$ with $\mu(A_{i})<\infty$ for all $i$.
${}^{\text{\faExternalLink}}$

Before we define products, we need some to know that limits of measurable
functions are measurable.

######  Lemma 4.1.

Let $X$ be a measurable space.

  1. 1.

Given a sequence of measurable functions $f_{n}:X\to[0,\infty]$ for
$n\in\mathbb{N}$, the pointwise suprema and infima
$f(x\vcentcolon=\sup\\{f_{n}(x)\\}_{n}$ and
$g(x\vcentcolon=\inf\\{f_{n}(x)\\}_{n}$ are measurable.
${}^{\text{\faExternalLink}}$

  2. 2.

Given a sequence of measurable functions $f_{n}:X\to[0,\infty]$ for
$n\in\mathbb{N}$ that converge pointwise to a function $f$, we can conclude
that $f$ is measurable. ${}^{\text{\faExternalLink}}$

  3. 3.

Let $Y$ be a metric space. Given a sequence of measurable functions
$f_{n}:X\to Y$ for $n\in\mathbb{N}$ that converge pointwise to a function $f$,
we can conclude that $f$ is measurable. ${}^{\text{\faExternalLink}}$

######  Proof 4.2.

For part 1, note that the collection of intervals $[0,x)$ generate the
$\upsigma$-algebra on $[0,\infty]$, as do the intervals $(x,\infty]$. The
conclusion follows from the fact that measurable sets are closed under
countable unions and observing that
$f^{-1}([0,x))=\bigcup_{n}f_{n}^{-1}([0,x))$ and
$g^{-1}((x,\infty])=\bigcup_{n}f_{n}^{-1}((x,\infty])$

Part 2 follows by observing that $f(x)=\liminf_{n}f_{n}(x)=\sup_{n}\inf_{m\geq
n}f_{m}(x)$, and applying both claims in part 1.

For part 3, let $C$ be a closed set in $Y$. The function
$d({-},C):Y\to[0,\infty]$ that assigns to each point the (minimal) distance to
$C$ is continuous. Therefore, we know that $h(x)\vcentcolon=d(f(x),C)$ is the
limit of the measurable functions $d(f_{n}(x),C)$ as $n\to\infty$. By part 2
we know that $h$ is measurable. Therefore $f^{-1}(C)=h^{-1}(\\{0\\})$ is
measurable (the equality holds because $C$ is closed).

If $X$ and $Y$ are measurable spaces, the $\upsigma$-algebra on $X\times Y$ is
the smallest $\upsigma$-algebra that make the projection $X\times Y\to X$ and
$X\times Y\to Y$ measurable. ${}^{\text{\faExternalLink}}$ Alternatively, it
can be characterized as the $\upsigma$-algebra generated by sets of the form
$A\times B$ for measurable $A\subseteq X$ and $B\subseteq Y$.
${}^{\text{\faExternalLink}}$

For the rest of this section, $\mu$ is a $\upsigma$-finite measure on $X$ and
$\nu$ is a $\upsigma$-finite measure on $Y$. For a set $A\subseteq X\times Y$
we write $A_{x}=\\{y\in Y\mid(x,y)\in A\\}$ for a slice of $Y$. In Lean, this
is written as prod.mk x ⁻¹' A. We want to define the product measure evaluated
at $A$ as an integral over the volume of the slices of $A$. To make sure that
this makes sense, we need to prove that this is a measurable function.
${}^{\text{\faExternalLink}}$

⬇

lemma measurable_measure_prod_mk_left [sigma_finite ν] {A : set (X × Y)}

(hA : is_measurable A) : measurable (λ x, ν (prod.mk x ⁻¹' A))

This lemma crucially depends on the fact that $\nu$ is $\upsigma$-finite, but
we omit the proof here. We can now define the product measure $\mu\times\nu$
on $X\times Y$ as ${}^{\text{\faExternalLink}}$

$\displaystyle(\mu\times\nu)(A)$
$\displaystyle=\int^{-}\nu(A_{x})\,\mathrm{d}\mu(x)$ (1)

It is not hard to see that $(\mu\times\nu)(A\times B)=\mu(A)\nu(B)$ for
measurable $A\subseteq X$ and $B\subseteq Y$ ${}^{\text{\faExternalLink}}$ and
that $\mu\times\nu$ is itself $\upsigma$-finite. ${}^{\text{\faExternalLink}}$

Also, when we pushforward the measure $\mu\times\nu$ across the map $X\times
Y\to Y\times X$ that swaps the coordinates, we get the measure $\nu\times\mu$
${}^{\text{\faExternalLink}}$ (this equality is easily checked because both
measures are equal on rectangles). This immediately gives the symmetric
version of (1): ${}^{\text{\faExternalLink}}$

$(\mu\times\nu)(A)=\int^{-}\mu(A^{y})\,\mathrm{d}\nu(y),$

where $A^{y}=\\{x\in X\mid(x,y)\in A\\}$.

For a function $f:X\times Y\to Z$ define $f_{x}:Y\to Z$ by
$f_{x}(y)\vcentcolon=f(x,y)$. If $Z=[0,\infty]$ let $I^{-}_{f}:X\to[0,\infty]$
be defined by
$I^{-}_{f}(x)\vcentcolon=\int^{-}_{Y}f_{x}\,\mathrm{d}\nu=\int^{-}_{Y}f(x,y)\,\mathrm{d}\nu(y)$.

We can now formulate Tonelli’s theorem.

######  Theorem 4.3 (Tonelli’s theorem).

Let $f:X\times Y\to[0,\infty]$ be a measurable function. Then
${}^{\text{\faExternalLink}}$ ${}^{\text{\faExternalLink}}$

$\int^{-}_{X\times
Y}f\,\mathrm{d}(\mu\times\nu)=\int^{-}_{X}\\!\\!\\!\int^{-}_{Y}f(x,y)\,\mathrm{d}\nu(y)\mathrm{d}\mu(x)=\int^{-}_{Y}\\!\\!\\!\int^{-}_{X}f(x,y)\,\mathrm{d}\mu(x)\mathrm{d}\nu(y),$

and all the functions in the integrals above are measurable.
${}^{\text{\faExternalLink}}$ ${}^{\text{\faExternalLink}}$

######  Proof 4.4.

We check the first equality and the measurability of $I^{-}_{f}$. The other
claims follow by symmetry. For both these statement we use _induction on
measurable functions into $[0,\infty]$_, ${}^{\text{\faExternalLink}}$ which
states that to prove a statement $P(f)$ for all measurable functions $f$ into
$[0,\infty]$, it is sufficient to show

  1. 1.

if $\chi_{A}$ is the characteristic function of a measurable set and
$c\in[0,\infty]$, we have $P(c\chi_{A})$;

  2. 2.

if $f_{1}$ and $f_{2}$ are measurable functions with $P(f_{1})$ and
$P(f_{2})$, then $P(f_{1}+f_{2})$;

  3. 3.

if $(f_{i})_{i}$ is a monotone sequence of measurable functions such that
$P(f_{i})$ for all $i$, we have $P(\sup_{i}f_{i})$.

We first prove that $I^{-}_{f}$ is measurable by induction on $f$.

In the induction base, if $f=c\chi_{A}$, then
$\int^{-}_{Y}f(x,y)\,\mathrm{d}\nu(y)=c\nu(A_{x})$, so the measurability
follows from measurable_measure_prod_mk_left. The two induction steps follow
from the additivity of the integral and the monotone convergence theorem.

We now prove the first equality in Theorem 4.3, also by induction on $f$. In
the induction base, if $f=c\chi_{A}$, then it is not hard to see that both
sides reduce to $c(\mu\times\nu)(A)$. The first induction step follows by
applying additivity thrice, and the second induction step follows by applying
the monotone convergence theorem thrice.

Fubini’s theorem (sometimes called Fubini–Tonelli’s theorem) states something
similar for the Bochner integral. However, it is a bit harder to state and
much harder to prove. For a function $f:X\times Y\to E$ define $I_{f}:X\to E$
by
$I_{f}(x)\vcentcolon=\int_{Y}f_{x}\,\mathrm{d}\nu=\int_{Y}f(x,y)\,\mathrm{d}\nu(y)$.

######  Theorem 4.5 (Fubini’s theorem for the Bochner integral).

Let $E$ be a second-countable Banach space and $f:X\times Y\to E$ be a
function.

  1. 1.

If $f$ is $\mu\times\nu$-a.e. measurable then $f$ is integrable iff the
following two conditions hold: ${}^{\text{\faExternalLink}}$

     * •

for almost all $x\in X$ the function $f_{x}$ is $\nu$-integrable;

     * •

The function $I_{\|f\|}$ is $\mu$-integrable.

  2. 2.

If $f$ is integrable, then ${}^{\text{\faExternalLink}}$
${}^{\text{\faExternalLink}}$

$\int_{X\times
Y}f\,\mathrm{d}(\mu\times\nu)=\int_{X}\\!\int_{Y}f(x,y)\,\mathrm{d}\nu(y)\mathrm{d}\mu(x)=\int_{Y}\\!\int_{X}f(x,y)\,\mathrm{d}\mu(x)\mathrm{d}\nu(y),$

Moreover, all the functions in the integrals above are a.e. measurable.
${}^{\text{\faExternalLink}}$ ${}^{\text{\faExternalLink}}$

Note that Part 1 also has a symmetric counterpart,
${}^{\text{\faExternalLink}}$ which we omit here. Note that the middle term in
Part 2 is just $\int_{X}I_{f}\,\mathrm{d}\mu(x)$

######  Proof 4.6.

Measurability. First suppose that $f$ is measurable. In this case, we show
that the function $I_{f}$ is measurable. We can approximate any measurable
function $f$ into a $E$ by a sequence $(s_{n})_{n}$ of simple functions
${}^{\text{\faExternalLink}}$ such that for all $z$ we have $\|s_{n}(z)\|\leq
2\|f(z)\|$ ${}^{\text{\faExternalLink}}$ and $s_{n}(z)\to f(z)$ as
$n\to\infty$. ${}^{\text{\faExternalLink}}$ Now define $g_{n}:X\to E$ by

$g_{n}(x)=\begin{cases}I_{s_{n}}(x)&\text{if $f_{x}$ is $\nu$-integrable}\\\
0&\text{otherwise.}\end{cases}$

Note that $g_{n}$ is similar to $I_{s_{n}}$, except that we set it to $0$
whenever $f_{x}$ is not integrable. This is required to ensure that $g_{n}$
converges to $I_{f}$ (see below). We first check that $g_{n}$ is measurable.
Note that the set

$\\{x\mid\text{$f_{x}$ is
$\nu$-integrable}\\}=\\{x\mid\textstyle\int_{Y}\|f(x,y)\|\,\mathrm{d}\nu(y)<\infty\\}$

is measurable, using Theorem 4.3. Therefore, to show that $g_{n}$ is
measurable, it suffices to show that $I_{s_{n}}$ is measurable, which is true,
since it is a finite sum of functions of the form $x\mapsto c\nu(A_{x})$
(using that $s_{n}$ is simple).

Secondly, we check that $g_{n}$ converges to $I_{f}$ pointwise. Let $x\in X$.
If $f_{x}$ is not integrable, it is trivially true, so assume that $f_{x}$ is
integrable. Then $(s_{n})_{x}$ is integrable for all $n$, and by the dominated
convergence theorem $I_{s_{n}}(x)$ converges to $I_{f}(x)$.

We conclude that $I_{f}$ is measurable by Lemma 4.1.

Finally, if $f$ is $\mu\times\nu$-a.e. measurable, then it is not hard to show
that $I_{f}$ is $\mu$-a.e. measurable.

Integrability. We now prove Part 1. By Tonelli’s theorem, we know that $f$ is
$\mu\times\nu$-integrable iff $I^{-}_{\|f\|}$ is $\mu$-integrable. Note that
$I^{-}_{\|f\|}$ is almost the same as $I_{\|f\|}$. The difference is that when
$f_{x}$ is not integrable, $I_{\|f\|}(x)=0$ but $I^{-}_{\|f\|}=\infty$. This
means that if $I^{-}_{\|f\|}$ is $\mu$-integrable, then $f_{x}$ must almost
always be $\nu$-integrable (otherwise the integrand is infinite on a set of
positive measure) and $I_{\|f\|}$ must be $\mu$-integrable. For the other
direction in Part 1, if $f_{x}$ is almost always integrable, then
$I_{\|f\|}=I^{-}_{\|f\|}$ almost everywhere, so if the former is
$\mu$-integrable, then so is the latter.

Equality. To prove the first equality in Part 2, we use the following
_induction principle for integrable functions_. ${}^{\text{\faExternalLink}}$
It states that to prove a statement $P(f)$ for all $\tau$-integrable functions
$f:Z\to E$, it is sufficient to show

  * •

if $A$ is measurable with $\tau(A)<\infty$ and $c\in E$, then $P(c\chi_{A})$;

  * •

if $f_{1}$ and $f_{2}$ are $\tau$-integrable functions with $P(f_{1})$ and
$P(f_{2})$, then $P(f_{1}+f_{2})$;

  * •

If $f_{1}$ is integrable with $P(f_{1})$ and $f_{1}=f_{2}$ $\tau$-a.e. then
$P(f_{2})$.

  * •

The set $\\{f\in L^{1}(Z,\tau;E)\mid P(f)\\}$ is closed.

We now prove that

$\displaystyle\int_{X\times Y}f\,\mathrm{d}(\mu\times\nu)$
$\displaystyle=\int_{X}\\!\int_{Y}f(x,y)\,\mathrm{d}\nu(y)\mathrm{d}\mu(x)$
(2)

by induction on $f$.

  * •

If $f=c\chi_{A}$ then it is easy to see that both sides of (2) reduce to
$c\cdot(\mu\times\nu)(A)$.

  * •

It is clear that if (2) holds for $f_{1}$ and $f_{2}$, then it also holds for
$f_{1}+f_{2}$.

  * •

Suppose that (2) holds for $f_{1}$ and that $f_{1}=f_{2}$ almost everywhere.
Since integrals are defined up to a.e. equality, we know that

$\int_{X\times Y}f_{1}\,\mathrm{d}(\mu\times\nu)=\int_{X\times
Y}f_{2}\,\mathrm{d}(\mu\times\nu).$

It therefore suffices to show that

$\int_{X}\\!\int_{Y}f_{1}(x,y)\,\mathrm{d}\nu(y)\mathrm{d}\mu(x)=\int_{X}\\!\int_{Y}f_{2}(x,y)\,\mathrm{d}\nu(y)\mathrm{d}\mu(x).$

For this it is sufficient to show that $I_{f_{1}}(x)=I_{f_{2}}(x)$ for almost
all $x$. Since $f_{1}(z)=f_{2}(z)$ for almost all $z$, it is not hard to see
${}^{\text{\faExternalLink}}$ that for almost all $x$ we have that for almost
all $y$ the equality $f_{1}(x,y)=f_{2}(x,y)$ holds. From this we easily get
that $I_{f_{1}}(x)=I_{f_{2}}(x)$ for almost all $x$.

  * •

We need to show that the set of $f\in L^{1}(Z,\tau;E)$ for which (2) holds is
closed. We know that taking the integral of an $L^{1}$ function is a
continuous operation, ${}^{\text{\faExternalLink}}$ which means that both
sides of (2) are continuous in $f$, which means that the set where these
functions are equal is closed.

##  5 Existence of The Haar Measure

In this section, we define the left Haar measure, and discuss some design
decisions when formalizing these definitions. We also discuss how to obtain a
right Haar measure from this definition.

Throughout this section, we assume that G is a locally compact group, equipped
with the Borel $\upsigma$-algebra. We will write the group operation
multiplicatively. We will define the Haar measure and show that it is a left
invariant regular measure on G. In the formalization, all intermediate
definitions and results are given with weaker conditions on G, following the
design in mathlib that all results should be in the most general form (within
reason).

In Lean, the precise conditions on G are written as follows.

⬇

{G : Type*} [topological_space G] [t2_space G] [locally_compact_space G]

[group G] [measurable_space G] [borel_space G] [topological_group G]

The concept of a left invariant measure is defined as follows in mathlib.
${}^{\text{\faExternalLink}}$

⬇

def is_left_invariant (μ : set G → ennreal) : Prop :=

∀ (g : G) {A : set G} (h : is_measurable A), μ ((λ h, g * h) ⁻¹' A) = μ A

Note that the preimage (λ h, g * h) ⁻¹' A is equal to the image (λ h, g⁻¹ * h)
'' A. We use preimages for translations, since preimages are nicer to work
with. For example, the fact that (λ h, g * h) ⁻¹' A is measurable follows
directly from the fact that multiplication (on the left) is a measurable
function.

Next we give the definition of a regular measure ${}^{\text{\faExternalLink}}$

⬇

structure regular (μ : measure X) : Prop :=

(lt_top_of_is_compact : ∀ ⦃K : set X⦄, is_compact K → μ K < ⊤)

(outer_regular : ∀ ⦃A : set X⦄, is_measurable A →

(⨅ (U : set X) (h : is_open U) (h2 : A ⊆ U), μ U) ≤ μ A)

(inner_regular : ∀ ⦃U : set X⦄, is_open U →

μ U ≤ ⨆ (K : set X) (h : is_compact K) (h2 : K ⊆ U), μ K)

If μ is a regular measure, then the inequalities in the last two fields are
always equalities. This means that a measure μ is regular if it is finite on
compact sets, its value on a measurable sets A is equal to the infimum (⨅) of
its value on all open sets containing A, and finally its value on an open set
U is the supremum (⨆) of its values on all compacts subsets of U.

We are now ready to start the definition of the Haar measure. Given a compact
set K in G, we start by giving a rough approximation of the “size” of K by
comparing it to a reference set V, which is an open neighborhood of (1 : G).
We can consider all left translates (λ h, g * h) ⁻¹' V of V, which is an open
covering of K. Since K is compact, we only need finitely many left translates
of V to cover K. ${}^{\text{\faExternalLink}}$ Let index K V be the smallest
number of left-translates of V needed to cover K. This is often denoted
$(K:V)$. We did not use this in Lean code, since it conflicts with the typing-
notation in Lean. In Lean, this notion is defined for arbitrary sets K and V,
and it is defined to be 0 if there is no finite number of left translates
covering K: ${}^{\text{\faExternalLink}}$

⬇

def index (K V : set G) : ℕ :=

Inf (finset.card '' {t : finset G | K ⊆ ⋃ g ∈ t, (λ h, g * h) ⁻¹' V })

For the rest of this section, we fix K₀ as an arbitrary compact set with non-
empty interior (in mathlib this is denoted K₀ : positive_compacts G). We then
define a weighted version of the index: ${}^{\text{\faExternalLink}}$

⬇

def prehaar (K₀ U : set G) (K : compacts G) : ℝ :=

(index K U : ℝ) / index K₀ U

######  Lemma 5.1.

Denote prehaar K₀ U K by $h_{U}(K)$ (recall that K₀ is fixed). Then we have

  * •

$(K:U)\leq(K:K_{0})\cdot(K_{0}:U)$; ${}^{\text{\faExternalLink}}$

  * •

$0\leq h_{U}(K)\leq(K:K_{0})$; ${}^{\text{\faExternalLink}}$

  * •

$h_{U}(K_{0})=1$; ${}^{\text{\faExternalLink}}$

  * •

$h_{U}(xK)=h_{U}(K)$; ${}^{\text{\faExternalLink}}$

  * •

if $K\subseteq K^{\prime}$ then $h_{U}(K)\leq h_{U}(K^{\prime})$;
${}^{\text{\faExternalLink}}$

  * •

if $h_{U}(K\cup K^{\prime})\leq h_{U}(K)+h_{U}(K^{\prime})$
${}^{\text{\faExternalLink}}$ and equality holds if $KU^{-1}\cap
K^{\prime}U^{-1}=\emptyset$. ${}^{\text{\faExternalLink}}$

To define the left Haar measure, we next want to define the “limit” of this
quotient as U becomes a smaller and smaller open neighborhoods of 1. This is
not an actual limit, but we will emulate it by constructing a product space
that contains all these functions, and then use a compactness argument to find
a “limit” in a large product space.

Consider the product

$\prod_{K\subseteq G\text{ compact}}[0,(K:K_{0})]$

In Lean this is defined as a subspace of the topological space compacts G → ℝ:
${}^{\text{\faExternalLink}}$

⬇

def haar_product (K₀ : set G) : set (compacts G → ℝ) :=

pi univ (λ K : compacts G, Icc 0 (index K K₀))

Here pi univ is the product of sets and Icc is an interval that is closed on
both sides.

Note that by Tychonoff’s theorem ${}^{\text{\faExternalLink}}$ haar_product K₀
is compact, and that every function prehaar K₀ U : compacts G → ℝ determines a
point in haar_product K₀. ${}^{\text{\faExternalLink}}$

Given a open neighborhood V of 1, we can define the collection of points
determined by prehaar K₀ U for all U ⊆ V and take its closure:

⬇

def cl_prehaar (K₀ : set G) (V : open_nhds_of (1 : G)) :

set (compacts G → ℝ) :=

closure (prehaar K₀ '' { U : set G | U ⊆ V ∧ is_open U ∧ (1 : G) ∈ U })

Now we claim that the intersection of cl_prehaar K₀ V for all open
neighborhoods V of 1 is non-empty.

⬇

lemma nonempty_Inter_cl_prehaar (K₀ : positive_compacts G) : nonempty

(haar_product K₀ ∩ ⋂ (V : open_nhds_of (1 : G)), cl_prehaar K₀ V)

######  Proof 5.2.

Since haar_product K₀ is compact, it is sufficient to show that if we have a
finite collection of open neighborhoods t : finset (open_nhds_of 1) the set
haar_product K₀ ∩ ⋂ (V ∈ t), cl_prehaar K₀ V is non-empty.
${}^{\text{\faExternalLink}}$ In this case we can explicitly give an element,
namely prehaar K₀ V₀, where V₀ = ⋂ (V ∈ t), V.

Finally, we can choose an arbitrary element in the set of the previous lemma,
which we call chaar K₀, since it measures the size of the compact sets of G:
${}^{\text{\faExternalLink}}$

⬇

def chaar (K₀ : positive_compacts G) (K : compacts G) : ℝ :=

classical.some (nonempty_Inter_cl_prehaar K₀) K

######  Lemma 5.3.

Denote chaar K₀ K by $h(K)$. Then we have

  * •

$0\leq h(K)$ ${}^{\text{\faExternalLink}}$ and $h(\emptyset)=0$
${}^{\text{\faExternalLink}}$ and $h(K_{0})=1$; ${}^{\text{\faExternalLink}}$

  * •

$h(xK)=h(K)$; ${}^{\text{\faExternalLink}}$

  * •

if $K\subseteq K^{\prime}$ then $h(K)\leq h(K^{\prime})$ (monotonicity);
${}^{\text{\faExternalLink}}$

  * •

if $h(K\cup K^{\prime})\leq h(K)+h(K^{\prime})$ (subadditivity)
${}^{\text{\faExternalLink}}$ and equality holds if $K\cap
K^{\prime}=\emptyset$ (additivity). ${}^{\text{\faExternalLink}}$

The idea in the proof is that the projections $f\mapsto f(K)$ are continuous
functions. Since these statements in this lemma hold for all $h_{U}$ by Lemma
5.1, they also hold for each point in each set cl_prehaar K₀ V, and therefore
for $h$.

This function chaar K₀ measures the size of the compact sets of G. It has the
properties of a _content_ on the compact sets, which is an additive,
subadditive and monotone function into the nonnegative reals [11, §53]. From
this content we can define the Haar measure in three steps.

First, given an arbitrary content, we can obtain its associated _inner
content_ on the open sets, ${}^{\text{\faExternalLink}}$

⬇

def inner_content (h : compacts G → ennreal) (U : opens G) : ennreal :=

⨆ (K : compacts G) (h : K ⊆ U), h K

This inner content is monotone ${}^{\text{\faExternalLink}}$ and countably
subadditive. ${}^{\text{\faExternalLink}}$ Also note that for every set K that
is both compact and open, we have inner_content h K = h K.
${}^{\text{\faExternalLink}}$

Second, given an arbitrary inner content ν, we can obtain its associated outer
measure μ ${}^{\text{\faExternalLink}}$ which is given by μ A = ⨅ (U : set G)
(hU : is_open U) (h : A ⊆ U), ν A. ${}^{\text{\faExternalLink}}$

For open sets U we have that μ U = ν U. ${}^{\text{\faExternalLink}}$ Suppose
that the inner content ν comes from the content h. We have observed that μ
agrees with ν on their common domain (the open sets), and that ν agrees with h
on their common domain (the compact open sets). One might be tempted to
conclude that μ agrees with h on their common domain (the compact sets). This
is implicitly claimed in Gleason [9], since the same name is used for these
three functions. However, this is not necessarily the case [11, p. 233]. The
best we can say in general is that for compact K we have μ (interior K) ≤ h K
≤ μ K ${}^{\text{\faExternalLink}}$ ${}^{\text{\faExternalLink}}$

If we apply these two steps to the function h = chaar K₀ we obtain the Haar
outer measure haar_outer_measure K₀ on G. ${}^{\text{\faExternalLink}}$ Next,
we show that all Borel measurable sets on G are Carathéodory measurable w.r.t.
haar_outer_measure K₀. ${}^{\text{\faExternalLink}}$ This gives the _left Haar
measure_. ${}^{\text{\faExternalLink}}$ We also scale the Haar measure so that
it assigns measure 1 to K₀.

⬇

def haar_measure (K₀ : positive_compacts G) : measure G :=

(haar_outer_measure K₀ K₀.1)⁻¹ •

(haar_outer_measure K₀).to_measure (haar_caratheodory_measurable K₀)

######  Theorem 5.4.

Let $\mu$ be the left Haar measure on $G$, defined above. Then $\mu$ is a left
invariant ${}^{\text{\faExternalLink}}$ and regular
${}^{\text{\faExternalLink}}$ measure satisfying $\mu(K_{0})=1$.
${}^{\text{\faExternalLink}}$

We will show in Section 6 that the Haar measure is unique, up to
multiplication determined by a constant. We finish this section by proving
some properties about left invariant regular measures.

######  Theorem 5.5.

Let $\mu$ be a nonzero left invariant regular measure on $G$.

  * •

If $U$ is a nonempty open set, the $\mu(U)>0$ ${}^{\text{\faExternalLink}}$

  * •

If $f:G\to\mathbb{R}$ is a nonnegative continuous function, not identically
equal to 0. Then $\int^{-}f\,\mathrm{d}\mu>0$. ${}^{\text{\faExternalLink}}$

In this section we have only discussed the left Haar measure, which is left
invariant. One can similarly define the notion of right invariance for a
measure. We can easily translate between these two notions. For a measure
$\mu$ define the measure $\check{\mu}$ by $\check{\mu}(A)=\mu(A^{-1})$.
${}^{\text{\faExternalLink}}$

######  Theorem 5.6.

  * •

The operation $\mu\mapsto\check{\mu}$ is involutive.
${}^{\text{\faExternalLink}}$

  * •

$\mu$ is left invariant iff $\check{\mu}$ is right invariant.
${}^{\text{\faExternalLink}}$

  * •

$\mu$ is regular iff $\check{\mu}$ is regular. ${}^{\text{\faExternalLink}}$

Theorem 5.6 shows that if $\mu$ is the left Haar measure on $G$, then
$\check{\mu}$ is a right Haar measure on $G$ (i.e. a nonzero regular right
invariant measure).

##  6 Uniqueness of the Haar measure

In this section we will show that the Haar measure is unique, up to
multiplication by a constant. For this proof, we followed the proof in Halmos
[11, §59-60]. We will compare our proof with the proof given in Halmos at the
end of the section.

Let $G$ be a second-countable locally compact group. The main ingredient in
the proof is that if we have two left invariant measures $\mu$ and $\nu$ on
$G$, we can transform expressions involving $\mu$ into expressions involving
$\nu$ by applying a transformation to $G\times G$ that preserves the measure
$\mu\times\nu$. We need Tonelli’s theorem to compute the integrals in this
product. Because $G$ is second countable, the product $\upsigma$-algebra on
$G\times G$ coincides with the Borel $\upsigma$-algebra.
${}^{\text{\faExternalLink}}$

Suppose $\mu$ and $\nu$ are left invariant and regular measures on $G$. Since
$G$ is second-countable, this also means that $\mu$ and $\nu$ are
$\upsigma$-finite. ${}^{\text{\faExternalLink}}$

We first show that $(x,y)\mapsto(x,xy)$ and $(x,y)\mapsto(yx,x^{-1})$ are
measure-preserving transformations.

######  Lemma 6.1.

Let $\mu$ and $\nu$ be left invariant regular measures on $G$, then the
transformations $S,T:G\times G\to G\times G$ given by
$S(x,y)\vcentcolon=(x,xy)$ and $T(x,y)\vcentcolon=(yx,x^{-1})$ preserve the
measure $\mu\times\nu$, i.e.
$S_{*}(\mu\times\nu)=\mu\times\nu=T_{*}(\mu\times\nu)$.
${}^{\text{\faExternalLink}}$ ${}^{\text{\faExternalLink}}$

######  Proof 6.2.

It suffices to show that the measures are equal on measurable rectangles,
since these generate the $\upsigma$-algebra on $G\times G$. Let $A\times
B\subseteq G\times G$ be a measurable rectangle. For $S$ we compute:

$\displaystyle S_{*}(\mu\times\nu)(A\times B)$
$\displaystyle=(\mu\times\nu)(S^{-1}(A\times B))$
$\displaystyle=\int^{-}\nu(S(x,{-})^{-1}(A\times B))\,\mathrm{d}\mu(x)$
$\displaystyle=\int^{-}\chi_{A}(x)\nu(x^{-1}B)\,\mathrm{d}\mu(x)$
$\displaystyle=\int^{-}\chi_{A}(x)\nu(B)\,\mathrm{d}\mu(x)=\mu(A)\nu(B)=(\mu\times\nu)(A\times
B).$

Note that $S$ is an equivalence with inverse $S^{-1}(x,y)=(x,x^{-1}y)$. If we
define $R(x,y)\vcentcolon=(y,x)$, we saw in Section 4 that
$R_{*}(\mu\times\nu)=\nu\times\mu$. The claim that $T$ preserves measure now
follows from the observation that $T=S^{-1}RSR$, which is easy to check.

For measurable sets $A$ its left translates have the same measure:
$\mu(xA)=\mu(A)$. This might not be true right translates $\mu(Ax)$, but we
can say the following [11, §59, Th. D].

######  Lemma 6.3.

Let $\mu$ be a left invariant regular measure on $G$ and suppose that
$\mu(A)>0$ for a measurable set $A\subseteq G$. Then $\mu(A^{-1})>0$
${}^{\text{\faExternalLink}}$ and $\mu(Ax)>0$ ${}^{\text{\faExternalLink}}$
for $x\in G$. Furthermore, the map $f(x)\vcentcolon=\mu(Ax)$ is measurable.
${}^{\text{\faExternalLink}}$

######  Proof 6.4.

Let $S$ and $T$ be as in Lemma 6.1. For the first claim, we will show that
$\mu(A^{-1})=0$ implies that $\mu(A)=0$. It suffices to show that
$(\mu\times\mu)(A\times A)=0$, which we can compute using Lemma 6.1:

$\displaystyle(\mu\times\mu)(A\times A)$
$\displaystyle=(\mu\times\mu)(T^{-1}(A\times A))$
$\displaystyle=\int^{-}\mu((T^{-1}(A\times A))^{y})\,\mathrm{d}\mu(y)$
$\displaystyle=\int^{-}\mu(y^{-1}A\cap
A^{-1})\,\mathrm{d}\mu(y)\leq\int^{-}\mu(A^{-1})\,\mathrm{d}\mu(y)=0.$

The second claim now easily follows, since $\mu(A)>0$ implies that
$\mu(Ax)=\mu((xA^{-1})^{-1})>0$.

For the final claim, it is not hard to see that $\mu(Ax)=\mu((S^{-1}(G\times
A)^{x})$, which is measurable by the symmetric version of
measurable_measure_prod_mk_left from Section 4.

The following is a technical lemma that allows us to rewrite $\nu$-integrals
into $\mu$-integrals. This is the key lemma to show the uniqueness of the Haar
measure. [11, §60, Th. A].

######  Lemma 6.5.

Let $\mu$ and $\nu$ be a left invariant regular measures on $G$, let
$K\subseteq G$ be compact with $\nu(K)>0$, and suppose that $f:G\to[0,\infty]$
is measurable. Then ${}^{\text{\faExternalLink}}$

$\mu(K)\cdot\int^{-}\frac{f(y^{-1})}{\nu(Ky)}\,\mathrm{d}\nu(y)=\int^{-}f\,\mathrm{d}\mu.$

######  Proof 6.6.

First note that $0<\nu(Ky)<\infty$ for any $y$. The first inequality follows
from Lemma 6.3 and the second inequality from the fact that $\nu$ is regular
and $Kx^{-1}$ is compact. Let $g(y)\vcentcolon=\frac{f(y^{-1})}{\nu(Ky)}$,
then by Lemma 6.3, $g$ is measurable. Now we compute

$\displaystyle\mu(K)\cdot\int^{-}g(y)\,\mathrm{d}\nu(y)$
$\displaystyle=\int^{-}\chi_{K}(x)\,\mathrm{d}\mu(x)\cdot\int^{-}g(y)\,\mathrm{d}\nu(y)$
$\displaystyle=\int^{-}\\!\\!\\!\int^{-}\chi_{K}(x)g(y)\,\mathrm{d}\nu(y)\,\mathrm{d}\mu(x)$
$\displaystyle=\int^{-}\\!\\!\\!\int^{-}\chi_{K}(yx)g(x^{-1})\,\mathrm{d}\nu(y)\,\mathrm{d}\mu(x)$
(by Lemma 6.1) $\displaystyle=\int^{-}\nu(Kx^{-1})g(x^{-1})\,\mathrm{d}\mu(x)$
$\displaystyle=\int^{-}f(x)\,\mathrm{d}\mu(x).$

As a consequence, we get the uniqueness of Haar measure: every left invariant
measure is a multiple of Haar measure.

######  Theorem 6.7.

Let $\nu$ be a left invariant regular measure and $K_{0}$ be a compact set
with non-empty interior. If $\mu$ is the Haar measure on $G$ with
$\mu(K_{0})=1$, then $\nu=\nu(K_{0})\cdot\mu$. ${}^{\text{\faExternalLink}}$

In the code, this theorem is stated as follows (in the formalization we assume
$\mu$ is $\upsigma$-finite instead of regular):

⬇

theorem haar_measure_unique [sigma_finite μ] (hμ : is_left_invariant μ)

(K₀ : positive_compacts G) : μ = μ K₀ • haar_measure K₀

######  Proof 6.8.

Let $A$ be any measurable set. The result follows from the following
computation, where we apply Lemma 6.5 twice, once with measures $(\nu,\mu)$
and once with measures $(\mu,\mu)$:

$\displaystyle\nu(A)$
$\displaystyle=\int^{-}\chi_{A}\,\mathrm{d}\nu=\nu(K_{0})\cdot\int^{-}\frac{\chi_{A}(y^{-1})}{\mu(K_{0}y)}\,\mathrm{d}\mu(y)$
$\displaystyle=\nu(K_{0})\cdot\mu(K_{0})\cdot\int^{-}\frac{\chi_{A}(y^{-1})}{\mu(K_{0}y)}\,\mathrm{d}\mu(y)=\nu(K_{0})\cdot\int^{-}\chi_{A}\,\mathrm{d}\mu=\nu(K_{0})\cdot\mu(A).$

For this proof we followed Halmos [11, §59-60], but there are some
differences. Halmos gives a more general version of Lemma 6.5, for an
arbitrary measurable group, while we did it for a second-countable locally
compact group equipped with the Borel $\upsigma$-algebra (which forms a
measurable group). There are other proofs, like in Cohn [3, Theorem 9.2.6],
that do not require $G$ to be second countable. Another difference between our
and Halmos’ proof is that we assume that $K$ is compact, while Halmos assumes
that $K$ is measurable with $\nu(K)<\infty$. However, in the proof he
implicitly uses that also $\nu(Ky)<\infty$, a fact that is not justified in
the text, and that I was unable to prove from the assumption that
$\nu(K)<\infty$. At this point I do not know whether this claim is true or
not. Lemma 6.3 claims something similar, namely that if $\nu(K)>0$ then
$\nu(Ky)>0$, but the proof of this claim does not work to show finiteness of
$\nu(Ky)$. We patched this gap by assuming that $K$ is compact and $\nu$ is
regular, which implies that $\nu(Ky)<\infty$ because $Ky$ is also compact.

##  7 Concluding Thoughts

The formalization of product measures is about 900 lines of code, and the
formalization of Haar measure is about 1300 lines of code (including blank
lines and comments). The proofs of these concepts use a wide variety of
techniques, from the reasoning in Banach spaces for Fubini’s theorem, to
topological compactness arguments in the existence proof of the Haar measure,
to the calculcational proofs in the uniqueness of the Haar measure. This
formalization shows that these different proof techniques can be used and
combined effectively in mathlib to formalize graduate level mathematics.

This work can be extended in various ways. One interesting project would be to
prove the uniqueness for groups that need not be second countable. This should
not be too difficult, but requires a version of Fubini’s theorem for compactly
supported functions on locally compact Hausdorff spaces. Another project would
be too explore the _modular function_ , which describes how the left and the
right Haar measures differ on a locally compact group. Furthermore, the Haar
measure is used as a tool in many areas of mathematics, and it would be
interesting to investigate which of these topics are now amenible to
formalization, with the Haar measure as new tool in our toolbelt.

One area that should be feasible to formalize is abstract harmonic analysis.
Abstract harmonic analysis is the area of analysis on topological groups,
usually locally compact groups. One of the core ideas is to generalize the
Fourier transform to an arbitrary locally compact abelian group. The special
case of the continuous Fourier transform has been formalized in HOL4 [10], but
the abstract Fourier transform has never been formalized. One specific goal
could be to formallize _Pontryagin duality_. For a locally compact abelian
group $G$ we can define the _Pontryagin dual_
$\widehat{G}\vcentcolon=\operatorname{Hom}(G,T)$ consisting of the continuous
group homomorphisms from $G$ to the circle group $T$. Then Pontryagin duality
states that the canonical map $G\to\widehat{\widehat{G}}$ (given by the
evaluation function) is an isomorphism. More ambitious targets include
representation theory of compact groups, Peter–Weyl theorem and Weyl’s
integral formula for compact Lie groups.

In mathlib we have not just defined binary product measures, but also finitary
product measures, ${}^{\text{\faExternalLink}}$ which can be used to define
integrals over $\mathbb{R}^{n}$. In mathlib this is done by defining a measure
on the product space Π i : ι, X i.

⬇

def measure.pi {ι : Type*} [fintype ι] {X : ι → Type*}

[∀ i, measurable_space (X i)] (μ : ∀ i, measure (X i)) :

measure (Π i, X i)

The definition is conceptually very simple, since you just iterate the
construction of binary product measures, but in practice it is quite tricky to
do it in a way that is convenient to use. For example, in a complicated proof,
you do not want to worry about the fact that the spaces $X\times(Y\times Z)$
and $(X\times Y)\times Z$ are not exactly the same, just equivalent. One open
question is whether we can formulate Fubini’s theorem for finitary product
measures in a way that is convenient to use. It would be inconvenient to
rewrite a finitary product of measures into a binary product in the desired
way, and then apply Fubini’s theorem for binary product measures. We have an
idea that we expect to be more promising, which is to define a new kind
integral that only some variables in the input of a function. It takes a
function f : (Π i, π i) → E and integrates away the variables in a subset I.
The result is another function (Π i, π i) → E that is constant on all
variables in I:

⬇

def integrate_away (μ : ∀ i, measure (π i)) (I : finset ι)

(f : (Π i, π i) → E) : (Π i, π i) → E

This has not been incorporated in mathlib, but it is a promising experiment on
a separate branch. ${}^{\text{\faExternalLink}}$ If we denote integrate_away μ
I f as ∫⋯∫_I, f ∂μ, then the following is a convenient way to state Fubini’s
theorem for finitary product measures.

⬇

lemma integrate_away_union (f : (Π i, π i) → E) (I J : finset ι) :

disjoint I J → ∫⋯∫_I ∪ J, f ∂μ = ∫⋯∫_ I, ∫⋯∫_J, f ∂μ ∂μ

## References

  * [1] Jeremy Avigad, Johannes Hölzl, and Luke Serafin.  A formally verified proof of the central limit theorem.  Journal of Automated Reasoning, 59(4):389–423, 2017.
  * [2] Aaron R. Coble.  Anonymity, information, and machine-assisted proof.  Technical Report UCAM-CL-TR-785, University of Cambridge, Computer Laboratory, July 2010.  URL: https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-785.pdf.
  * [3] Donald L. Cohn.  Measure Theory.  Birkhäuser Basel, 2 edition, 2013.
  * [4] Johan Commelin and Robert Y. Lewis.  Formalizing the ring of Witt vectors.  In Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2021, page 264–277, New York, NY, USA, 2021. Association for Computing Machinery.  URL: https://doi.org/10.1145/3437992.3439919, doi:10.1145/3437992.3439919.
  * [5] The mathlib Community.  The Lean mathematical library.  In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, page 367–381, New York, NY, USA, 2020. Association for Computing Machinery.  doi:10.1145/3372885.3373824.
  * [6] Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer.  The Lean Theorem Prover (system description).  CADE-25, pages 378–388, August 2015.
  * [7] Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, and Leonardo de Moura.  A metaprogramming framework for formal verification.  Proc. ACM Program. Lang., 1(ICFP):34:1–34:29, aug 2017.  doi:10.1145/3110278.
  * [8] Noboru Endou, Keiko Narita, and Yasunari Shidama.  The Lebesgue monotone convergence theorem.  Formalized Mathematics, 16(2):167–175, 2008.
  * [9] Jonathan Gleason.  Existence and uniqueness of Haar measure.  preprint, 2010.
  * [10] Yong Guan, Jie Zhang, Zhiping Shi, Yi Wang, and Yongdong Li.  Formalization of continuous Fourier transform in verifying applications for dependable cyber-physical systems.  Journal of Systems Architecture, 106:101707, 2020.  URL: http://www.sciencedirect.com/science/article/pii/S1383762120300011, doi:https://doi.org/10.1016/j.sysarc.2020.101707.
  * [11] Paul R. Halmos.  Measure theory.  Springer-Verlag New York, 1950.  doi:10.1007/978-1-4684-9440-2.
  * [12] John Harrison.  The HOL Light theory of Euclidean space.  Journal of Automated Reasoning, 50(2):173–190, 2013.  doi:10.1007/s10817-012-9250-9.
  * [13] Johannes Hölzl and Armin Heller.  Three chapters of measure theory in Isabelle/HOL.  In Interactive Theorem Proving, pages 135–151, Berlin, Heidelberg, 2011. Springer Berlin Heidelberg.
  * [14] Joe Hurd.  Formal verification of probabilistic algorithms.  Technical Report UCAM-CL-TR-566, University of Cambridge, Computer Laboratory, May 2003.  URL: https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-566.pdf.
  * [15] David R Lester.  Topology in PVS: Continuous mathematics with applications.  In Proceedings of the Second Workshop on Automated Formal Methods, AFM ’07, page 11–20, New York, NY, USA, 2007. Association for Computing Machinery.  doi:10.1145/1345169.1345171.
  * [16] Tarek Mhamdi, Osman Hasan, and Sofiène Tahar.  Formalization of measure theory and Lebesgue integration for probabilistic analysis in HOL.  ACM Trans. Embed. Comput. Syst., 12(1), January 2013.  doi:10.1145/2406336.2406349.
  * [17] Stefan Richter.  Formalizing integration theory with an application to probabilistic algorithms.  In Theorem Proving in Higher Order Logics, pages 271–286, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg.
  * [18] B.A.W. Spitters and E.E. van der Weegen.  Type classes for mathematics in type theory.  Mathematical Structures in Computer Science, 21:795–825, 2011.
  * [19] P. Wadler and S. Blott.  How to make ad-hoc polymorphism less ad hoc.  In Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’89, page 60–76, New York, NY, USA, 1989. Association for Computing Machinery.  URL: https://doi.org/10.1145/75277.75283, doi:10.1145/75277.75283.