mathlib3 documentation

measure_theory.measure.haar.basic

Haar measure #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we prove the existence and uniqueness (up to scalar multiples) of Haar measure for a locally compact Hausdorff topological group.

For the construction, we follow the write-up by Jonathan Gleason, Existence and Uniqueness of Haar Measure. This is essentially the same argument as in https://en.wikipedia.org/wiki/Haar_measure#A_construction_using_compact_subsets.

We construct the Haar measure first on compact sets. For this we define (K : U) as the (smallest) number of left-translates of U that are needed to cover K (index in the formalization). Then we define a function h on compact sets as lim_U (K : U) / (K₀ : U), where U becomes a smaller and smaller open neighborhood of 1, and K₀ is a fixed compact set with nonempty interior. This function is chaar in the formalization, and we define the limit formally using Tychonoff's theorem.

This function h forms a content, which we can extend to an outer measure and then a measure (haar_measure). We normalize the Haar measure so that the measure of K₀ is 1. We show that for second countable spaces any left invariant Borel measure is a scalar multiple of the Haar measure.

Note that μ need not coincide with h on compact sets, according to [halmos1950measure, ch. X, §53 p.233]. However, we know that h(K) lies between μ(Kᵒ) and μ(K), where denotes the interior.

Main Declarations #

References #

We put the internal functions in the construction of the Haar measure in a namespace, so that the chosen names don't clash with other declarations. We first define a couple of the functions before proving the properties (that require that G is a topological group).

noncomputable def measure_theory.measure.haar.index {G : Type u_1} [group G] (K V : set G) :

The index or Haar covering number or ratio of K w.r.t. V, denoted (K : V): it is the smallest number of (left) translates of V that is necessary to cover K. It is defined to be 0 if no finite number of translates cover K.

Equations
noncomputable def measure_theory.measure.haar.add_index {G : Type u_1} [add_group G] (K V : set G) :

additive version of measure_theory.measure.haar.index

Equations
noncomputable def measure_theory.measure.haar.prehaar {G : Type u_1} [group G] [topological_space G] (K₀ U : set G) (K : topological_space.compacts G) :

prehaar K₀ U K is a weighted version of the index, defined as (K : U)/(K₀ : U). In the applications K₀ is compact with non-empty interior, U is open containing 1, and K is any compact set. The argument K is a (bundled) compact set, so that we can consider prehaar K₀ U as an element of haar_product (below).

Equations

haar_product K₀ is the product of intervals [0, (K : K₀)], for all compact sets K. For all U, we can show that prehaar K₀ U ∈ haar_product K₀.

Equations

The closure of the collection of elements of the form prehaar K₀ U, for U open neighbourhoods of 1, contained in V. The closure is taken in the space compacts G → ℝ, with the topology of pointwise convergence. We show that the intersection of all these sets is nonempty, and the Haar measure on compact sets is defined to be an element in the closure of this intersection.

Equations

Lemmas about index #

theorem measure_theory.measure.haar.index_defined {G : Type u_1} [group G] [topological_space G] [topological_group G] {K V : set G} (hK : is_compact K) (hV : (interior V).nonempty) :
(n : ), n finset.card '' {t : finset G | K (g : G) (H : g t), (λ (h : G), g * h) ⁻¹' V}

If K is compact and V has nonempty interior, then the index (K : V) is well-defined, there is a finite set t satisfying the desired properties.

theorem measure_theory.measure.haar.add_index_defined {G : Type u_1} [add_group G] [topological_space G] [topological_add_group G] {K V : set G} (hK : is_compact K) (hV : (interior V).nonempty) :
(n : ), n finset.card '' {t : finset G | K (g : G) (H : g t), (λ (h : G), g + h) ⁻¹' V}

If K is compact and V has nonempty interior, then the index (K : V) is well-defined, there is a finite set t satisfying the desired properties.

theorem measure_theory.measure.haar.add_index_elim {G : Type u_1} [add_group G] [topological_space G] [topological_add_group G] {K V : set G} (hK : is_compact K) (hV : (interior V).nonempty) :
(t : finset G), (K (g : G) (H : g t), (λ (h : G), g + h) ⁻¹' V) t.card = measure_theory.measure.haar.add_index K V
theorem measure_theory.measure.haar.index_elim {G : Type u_1} [group G] [topological_space G] [topological_group G] {K V : set G} (hK : is_compact K) (hV : (interior V).nonempty) :
(t : finset G), (K (g : G) (H : g t), (λ (h : G), g * h) ⁻¹' V) t.card = measure_theory.measure.haar.index K V

Lemmas about prehaar #

Lemmas about haar_product #

Lemmas about chaar #

This is the "limit" of prehaar K₀ U K as U becomes a smaller and smaller open neighborhood of (1 : G). More precisely, it is defined to be an arbitrary element in the intersection of all the sets cl_prehaar K₀ V in haar_product K₀. This is roughly equal to the Haar measure on compact sets, but it can differ slightly. We do know that haar_measure K₀ (interior K) ≤ chaar K₀ K ≤ haar_measure K₀ K.

Equations

The function chaar interpreted in ℝ≥0, as a content

Equations

We only prove the properties for haar_content that we use at least twice below.

The Haar measure #

@[protected, instance]

The additive Haar measure is an additive Haar measure, i.e., it is invariant and gives finite mass to compact sets and positive mass to nonempty open sets.

@[protected, instance]

The Haar measure is a Haar measure, i.e., it is invariant and gives finite mass to compact sets and positive mass to nonempty open sets.

The additive Haar measure is unique up to scaling. More precisely: every σ-finite left invariant measure is a scalar multiple of the additive Haar measure. This is slightly weaker than assuming that μ is an additive Haar measure (in particular we don't require μ ≠ 0).

The Haar measure is unique up to scaling. More precisely: every σ-finite left invariant measure is a scalar multiple of the Haar measure. This is slightly weaker than assuming that μ is a Haar measure (in particular we don't require μ ≠ 0).

To show that an invariant σ-finite measure is regular it is sufficient to show that it is finite on some compact set with non-empty interior.

To show that an invariant σ-finite measure is regular it is sufficient to show that it is finite on some compact set with non-empty interior.

Steinhaus Theorem In any locally compact group G with a haar measure μ, for any measurable set E of positive measure, the set E / E is a neighbourhood of 1.

Steinhaus Theorem In any locally compact group G with a haar measure μ, for any measurable set E of positive measure, the set E - E is a neighbourhood of 0.