Haar measure
In this file we prove the existence 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 are needed to cover K (index in the formalization).
Then we define the Haar measure on compact sets as lim_U (K : U) / (K₀ : U),
where U ranges over open neighborhoods of 1, and K₀ is a fixed compact set with nonempty
interior. This is chaar in the formalization, and we prove that the limit exists by Tychonoff's
theorem.
The Haar measure on compact sets forms a content, which we can extend to an outer measure
(haar_outer_measure), and obtain the Haar measure from that (haar_measure).
We normalize the Haar measure so that the measure of K₀ is 1.
Main Declarations
haar_measure: the Haar measure on a locally compact Hausdorff group. This is a left invariant regular measure. It takes as argument a compact set of the group (with non-empty interior), and is normalized so that the measure of the given set is 1.haar_measure_self: the Haar measure is normalized.is_left_invariant_haar_measure: the Haar measure is left invariant.regular_haar_measure: the Haar measure is a regular measure.
References
- Paul Halmos (1950), Measure Theory, §53
- Jonathan Gleason, Existence and Uniqueness of Haar Measure
- Note: step 9, page 8 contains a mistake: the last defined
μdoes not extend theμon compact sets, see Halmos (1950) p. 233, bottom of the page. This makes some other steps (like step 11) invalid.
- Note: step 9, page 8 contains a mistake: the last defined
- https://en.wikipedia.org/wiki/Haar_measure
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).
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
- measure_theory.measure.haar.index K V = has_Inf.Inf (finset.card '' {t : finset G | K ⊆ ⋃ (g : G) (H : g ∈ t), (λ (h : G), g * h) ⁻¹' V})
def
measure_theory.measure.haar.prehaar
{G : Type u_1}
[group G]
[topological_space G] :
set G → set G → 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
theorem
measure_theory.measure.haar.prehaar_empty
{G : Type u_1}
[group G]
[topological_space G]
(K₀ : topological_space.positive_compacts G)
{U : set G} :
measure_theory.measure.haar.prehaar K₀.val U ⊥ = 0
theorem
measure_theory.measure.haar.prehaar_nonneg
{G : Type u_1}
[group G]
[topological_space G]
(K₀ : topological_space.positive_compacts G)
{U : set G}
(K : topological_space.compacts G) :
0 ≤ measure_theory.measure.haar.prehaar K₀.val U K
def
measure_theory.measure.haar.haar_product
{G : Type u_1}
[group G]
[topological_space G] :
set G → set (topological_space.compacts G → ℝ)
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
- measure_theory.measure.haar.haar_product K₀ = set.univ.pi (λ (K : topological_space.compacts G), set.Icc 0 ↑(measure_theory.measure.haar.index K.val K₀))
@[simp]
theorem
measure_theory.measure.haar.mem_prehaar_empty
{G : Type u_1}
[group G]
[topological_space G]
{K₀ : set G}
{f : topological_space.compacts G → ℝ} :
f ∈ measure_theory.measure.haar.haar_product K₀ ↔ ∀ (K : topological_space.compacts G), f K ∈ set.Icc 0 ↑(measure_theory.measure.haar.index K.val K₀)
def
measure_theory.measure.haar.cl_prehaar
{G : Type u_1}
[group G]
[topological_space G] :
set G → topological_space.open_nhds_of 1 → set (topological_space.compacts G → ℝ)
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.
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} :
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.index_elim
{G : Type u_1}
[group G]
[topological_space G]
[topological_group G]
{K V : set G} :
theorem
measure_theory.measure.haar.le_index_mul
{G : Type u_1}
[group G]
[topological_space G]
[topological_group G]
(K₀ : topological_space.positive_compacts G)
(K : topological_space.compacts G)
{V : set G} :
theorem
measure_theory.measure.haar.index_pos
{G : Type u_1}
[group G]
[topological_space G]
[topological_group G]
(K : topological_space.positive_compacts G)
{V : set G} :
(interior V).nonempty → 0 < measure_theory.measure.haar.index K.val V
theorem
measure_theory.measure.haar.index_mono
{G : Type u_1}
[group G]
[topological_space G]
[topological_group G]
{K K' V : set G} :
is_compact K' → K ⊆ K' → (interior V).nonempty → measure_theory.measure.haar.index K V ≤ measure_theory.measure.haar.index K' V
theorem
measure_theory.measure.haar.index_union_le
{G : Type u_1}
[group G]
[topological_space G]
[topological_group G]
(K₁ K₂ : topological_space.compacts G)
{V : set G} :
(interior V).nonempty → measure_theory.measure.haar.index (K₁.val ∪ K₂.val) V ≤ measure_theory.measure.haar.index K₁.val V + measure_theory.measure.haar.index K₂.val V
theorem
measure_theory.measure.haar.index_union_eq
{G : Type u_1}
[group G]
[topological_space G]
[topological_group G]
(K₁ K₂ : topological_space.compacts G)
{V : set G} :
theorem
measure_theory.measure.haar.mul_left_index_le
{G : Type u_1}
[group G]
[topological_space G]
[topological_group G]
{K : set G}
(hK : is_compact K)
{V : set G}
(hV : (interior V).nonempty)
(g : G) :
measure_theory.measure.haar.index ((λ (h : G), g * h) '' K) V ≤ measure_theory.measure.haar.index K V
theorem
measure_theory.measure.haar.is_left_invariant_index
{G : Type u_1}
[group G]
[topological_space G]
[topological_group G]
{K : set G}
(hK : is_compact K)
{V : set G}
(hV : (interior V).nonempty)
(g : G) :
measure_theory.measure.haar.index ((λ (h : G), g * h) '' K) V = measure_theory.measure.haar.index K V
Lemmas about prehaar
theorem
measure_theory.measure.haar.prehaar_le_index
{G : Type u_1}
[group G]
[topological_space G]
[topological_group G]
(K₀ : topological_space.positive_compacts G)
{U : set G}
(K : topological_space.compacts G) :
(interior U).nonempty → measure_theory.measure.haar.prehaar K₀.val U K ≤ ↑(measure_theory.measure.haar.index K.val K₀.val)
theorem
measure_theory.measure.haar.prehaar_pos
{G : Type u_1}
[group G]
[topological_space G]
[topological_group G]
(K₀ : topological_space.positive_compacts G)
{U : set G}
(hU : (interior U).nonempty)
{K : set G}
(h1K : is_compact K) :
theorem
measure_theory.measure.haar.prehaar_mono
{G : Type u_1}
[group G]
[topological_space G]
[topological_group G]
{K₀ : topological_space.positive_compacts G}
{U : set G}
(hU : (interior U).nonempty)
{K₁ K₂ : topological_space.compacts G} :
K₁.val ⊆ K₂.val → measure_theory.measure.haar.prehaar K₀.val U K₁ ≤ measure_theory.measure.haar.prehaar K₀.val U K₂
theorem
measure_theory.measure.haar.prehaar_self
{G : Type u_1}
[group G]
[topological_space G]
[topological_group G]
{K₀ : topological_space.positive_compacts G}
{U : set G} :
theorem
measure_theory.measure.haar.prehaar_sup_le
{G : Type u_1}
[group G]
[topological_space G]
[topological_group G]
{K₀ : topological_space.positive_compacts G}
{U : set G}
(K₁ K₂ : topological_space.compacts G) :
(interior U).nonempty → measure_theory.measure.haar.prehaar K₀.val U (K₁ ⊔ K₂) ≤ measure_theory.measure.haar.prehaar K₀.val U K₁ + measure_theory.measure.haar.prehaar K₀.val U K₂
theorem
measure_theory.measure.haar.prehaar_sup_eq
{G : Type u_1}
[group G]
[topological_space G]
[topological_group G]
{K₀ : topological_space.positive_compacts G}
{U : set G}
{K₁ K₂ : topological_space.compacts G} :
theorem
measure_theory.measure.haar.is_left_invariant_prehaar
{G : Type u_1}
[group G]
[topological_space G]
[topological_group G]
{K₀ : topological_space.positive_compacts G}
{U : set G}
(hU : (interior U).nonempty)
{K : topological_space.compacts G}
{g : G} :
measure_theory.measure.haar.prehaar K₀.val U (topological_space.compacts.map (λ (b : G), g * b) _ K) = measure_theory.measure.haar.prehaar K₀.val U K
Lemmas about haar_product
theorem
measure_theory.measure.haar.prehaar_mem_haar_product
{G : Type u_1}
[group G]
[topological_space G]
[topological_group G]
(K₀ : topological_space.positive_compacts G)
{U : set G} :
theorem
measure_theory.measure.haar.nonempty_Inter_cl_prehaar
{G : Type u_1}
[group G]
[topological_space G]
[topological_group G]
(K₀ : topological_space.positive_compacts G) :
The Haar measure on compact sets
def
measure_theory.measure.haar.chaar
{G : Type u_1}
[group G]
[topological_space G]
[topological_group G] :
The Haar measure on compact sets, defined to be an arbitrary element in the intersection of
all the sets cl_prehaar K₀ V in haar_product K₀.
Equations
theorem
measure_theory.measure.haar.chaar_mem_haar_product
{G : Type u_1}
[group G]
[topological_space G]
[topological_group G]
(K₀ : topological_space.positive_compacts G) :
theorem
measure_theory.measure.haar.chaar_mem_cl_prehaar
{G : Type u_1}
[group G]
[topological_space G]
[topological_group G]
(K₀ : topological_space.positive_compacts G)
(V : topological_space.open_nhds_of 1) :
theorem
measure_theory.measure.haar.chaar_nonneg
{G : Type u_1}
[group G]
[topological_space G]
[topological_group G]
(K₀ : topological_space.positive_compacts G)
(K : topological_space.compacts G) :
theorem
measure_theory.measure.haar.chaar_empty
{G : Type u_1}
[group G]
[topological_space G]
[topological_group G]
(K₀ : topological_space.positive_compacts G) :
theorem
measure_theory.measure.haar.chaar_self
{G : Type u_1}
[group G]
[topological_space G]
[topological_group G]
(K₀ : topological_space.positive_compacts G) :
measure_theory.measure.haar.chaar K₀ ⟨K₀.val, _⟩ = 1
theorem
measure_theory.measure.haar.chaar_mono
{G : Type u_1}
[group G]
[topological_space G]
[topological_group G]
{K₀ : topological_space.positive_compacts G}
{K₁ K₂ : topological_space.compacts G} :
K₁.val ⊆ K₂.val → measure_theory.measure.haar.chaar K₀ K₁ ≤ measure_theory.measure.haar.chaar K₀ K₂
theorem
measure_theory.measure.haar.chaar_sup_le
{G : Type u_1}
[group G]
[topological_space G]
[topological_group G]
{K₀ : topological_space.positive_compacts G}
(K₁ K₂ : topological_space.compacts G) :
measure_theory.measure.haar.chaar K₀ (K₁ ⊔ K₂) ≤ measure_theory.measure.haar.chaar K₀ K₁ + measure_theory.measure.haar.chaar K₀ K₂
theorem
measure_theory.measure.haar.chaar_sup_eq
{G : Type u_1}
[group G]
[topological_space G]
[topological_group G]
[t2_space G]
{K₀ : topological_space.positive_compacts G}
{K₁ K₂ : topological_space.compacts G} :
disjoint K₁.val K₂.val → measure_theory.measure.haar.chaar K₀ (K₁ ⊔ K₂) = measure_theory.measure.haar.chaar K₀ K₁ + measure_theory.measure.haar.chaar K₀ K₂
theorem
measure_theory.measure.haar.is_left_invariant_chaar
{G : Type u_1}
[group G]
[topological_space G]
[topological_group G]
{K₀ : topological_space.positive_compacts G}
{K : topological_space.compacts G}
{g : G} :
measure_theory.measure.haar.chaar K₀ (topological_space.compacts.map (λ (b : G), g * b) _ K) = measure_theory.measure.haar.chaar K₀ K
def
measure_theory.measure.haar.echaar
{G : Type u_1}
[group G]
[topological_space G]
[topological_group G] :
The function chaar interpreted in ennreal
Equations
- measure_theory.measure.haar.echaar K₀ K = ↑((λ (this : nnreal), this) ⟨measure_theory.measure.haar.chaar K₀ K, _⟩)
theorem
measure_theory.measure.haar.echaar_sup_le
{G : Type u_1}
[group G]
[topological_space G]
[topological_group G]
{K₀ : topological_space.positive_compacts G}
(K₁ K₂ : topological_space.compacts G) :
measure_theory.measure.haar.echaar K₀ (K₁ ⊔ K₂) ≤ measure_theory.measure.haar.echaar K₀ K₁ + measure_theory.measure.haar.echaar K₀ K₂
The variant of chaar_sup_le for echaar
theorem
measure_theory.measure.haar.echaar_mono
{G : Type u_1}
[group G]
[topological_space G]
[topological_group G]
{K₀ : topological_space.positive_compacts G}
⦃K₁ K₂ : topological_space.compacts G⦄ :
K₁.val ⊆ K₂.val → measure_theory.measure.haar.echaar K₀ K₁ ≤ measure_theory.measure.haar.echaar K₀ K₂
The variant of chaar_mono for echaar
The Haar outer measure
def
measure_theory.measure.haar_outer_measure
{G : Type u_1}
[group G]
[topological_space G]
[t2_space G]
[topological_group G] :
The Haar outer measure on G. It is not normalized, and is mainly used to construct
haar_measure, which is a normalized measure.
theorem
measure_theory.measure.haar_outer_measure_eq_infi
{G : Type u_1}
[group G]
[topological_space G]
[t2_space G]
[topological_group G]
(K₀ : topological_space.positive_compacts G)
(A : set G) :
⇑(measure_theory.measure.haar_outer_measure K₀) A = ⨅ (U : set G) (hU : is_open U) (h : A ⊆ U), measure_theory.inner_content (measure_theory.measure.haar.echaar K₀) ⟨U, hU⟩
theorem
measure_theory.measure.chaar_le_haar_outer_measure
{G : Type u_1}
[group G]
[topological_space G]
[t2_space G]
[topological_group G]
{K₀ : topological_space.positive_compacts G}
(K : topological_space.compacts G) :
↑((λ (this : nnreal), this) ⟨measure_theory.measure.haar.chaar K₀ K, _⟩) ≤ ⇑(measure_theory.measure.haar_outer_measure K₀) K.val
theorem
measure_theory.measure.haar_outer_measure_of_is_open
{G : Type u_1}
[group G]
[topological_space G]
[t2_space G]
[topological_group G]
{K₀ : topological_space.positive_compacts G}
(U : set G)
(hU : is_open U) :
⇑(measure_theory.measure.haar_outer_measure K₀) U = measure_theory.inner_content (λ (K : topological_space.compacts G), ↑((λ (this : nnreal), this) ⟨measure_theory.measure.haar.chaar K₀ K, _⟩)) ⟨U, hU⟩
theorem
measure_theory.measure.haar_outer_measure_le_chaar
{G : Type u_1}
[group G]
[topological_space G]
[t2_space G]
[topological_group G]
{K₀ : topological_space.positive_compacts G}
{U : set G}
(hU : is_open U)
(K : topological_space.compacts G) :
U ⊆ K.val → ⇑(measure_theory.measure.haar_outer_measure K₀) U ≤ ↑((λ (this : nnreal), this) ⟨measure_theory.measure.haar.chaar K₀ K, _⟩)
theorem
measure_theory.measure.haar_outer_measure_exists_open
{G : Type u_1}
[group G]
[topological_space G]
[t2_space G]
[topological_group G]
{K₀ : topological_space.positive_compacts G}
{A : set G}
(hA : ⇑(measure_theory.measure.haar_outer_measure K₀) A < ⊤)
{ε : nnreal} :
0 < ε → (∃ (U : topological_space.opens G), A ⊆ ↑U ∧ ⇑(measure_theory.measure.haar_outer_measure K₀) ↑U ≤ ⇑(measure_theory.measure.haar_outer_measure K₀) A + ↑ε)
theorem
measure_theory.measure.haar_outer_measure_exists_compact
{G : Type u_1}
[group G]
[topological_space G]
[t2_space G]
[topological_group G]
{K₀ : topological_space.positive_compacts G}
{U : topological_space.opens G}
(hU : ⇑(measure_theory.measure.haar_outer_measure K₀) ↑U < ⊤)
{ε : nnreal} :
0 < ε → (∃ (K : topological_space.compacts G), K.val ⊆ ↑U ∧ ⇑(measure_theory.measure.haar_outer_measure K₀) ↑U ≤ ⇑(measure_theory.measure.haar_outer_measure K₀) K.val + ↑ε)
theorem
measure_theory.measure.haar_outer_measure_caratheodory
{G : Type u_1}
[group G]
[topological_space G]
[t2_space G]
[topological_group G]
{K₀ : topological_space.positive_compacts G}
(A : set G) :
(measure_theory.measure.haar_outer_measure K₀).caratheodory.is_measurable A ↔ ∀ (U : topological_space.opens G), ⇑(measure_theory.measure.haar_outer_measure K₀) (↑U ∩ A) + ⇑(measure_theory.measure.haar_outer_measure K₀) (↑U \ A) ≤ ⇑(measure_theory.measure.haar_outer_measure K₀) ↑U
theorem
measure_theory.measure.one_le_haar_outer_measure_self
{G : Type u_1}
[group G]
[topological_space G]
[t2_space G]
[topological_group G]
{K₀ : topological_space.positive_compacts G} :
1 ≤ ⇑(measure_theory.measure.haar_outer_measure K₀) K₀.val
theorem
measure_theory.measure.haar_outer_measure_pos_of_is_open
{G : Type u_1}
[group G]
[topological_space G]
[t2_space G]
[topological_group G]
{K₀ : topological_space.positive_compacts G}
{U : set G} :
is_open U → U.nonempty → 0 < ⇑(measure_theory.measure.haar_outer_measure K₀) U
theorem
measure_theory.measure.haar_outer_measure_self_pos
{G : Type u_1}
[group G]
[topological_space G]
[t2_space G]
[topological_group G]
{K₀ : topological_space.positive_compacts G} :
0 < ⇑(measure_theory.measure.haar_outer_measure K₀) K₀.val
theorem
measure_theory.measure.haar_outer_measure_lt_top_of_is_compact
{G : Type u_1}
[group G]
[topological_space G]
[t2_space G]
[topological_group G]
[locally_compact_space G]
{K₀ : topological_space.positive_compacts G}
{K : set G} :
is_compact K → ⇑(measure_theory.measure.haar_outer_measure K₀) K < ⊤
theorem
measure_theory.measure.haar_caratheodory_measurable
{G : Type u_1}
[group G]
[topological_space G]
[t2_space G]
[topological_group G]
[S : measurable_space G]
[borel_space G]
(K₀ : topological_space.positive_compacts G) :
The Haar measure
def
measure_theory.measure.haar_measure
{G : Type u_1}
[group G]
[topological_space G]
[t2_space G]
[topological_group G]
[S : measurable_space G]
[borel_space G] :
the Haar measure on G, scaled so that haar_measure K₀ K₀ = 1.
Equations
theorem
measure_theory.measure.haar_measure_apply
{G : Type u_1}
[group G]
[topological_space G]
[t2_space G]
[topological_group G]
[S : measurable_space G]
[borel_space G]
{K₀ : topological_space.positive_compacts G}
{s : set G} :
theorem
measure_theory.measure.is_left_invariant_haar_measure
{G : Type u_1}
[group G]
[topological_space G]
[t2_space G]
[topological_group G]
[S : measurable_space G]
[borel_space G]
(K₀ : topological_space.positive_compacts G) :
theorem
measure_theory.measure.haar_measure_self
{G : Type u_1}
[group G]
[topological_space G]
[t2_space G]
[topological_group G]
[S : measurable_space G]
[borel_space G]
[locally_compact_space G]
{K₀ : topological_space.positive_compacts G} :
⇑(measure_theory.measure.haar_measure K₀) K₀.val = 1
theorem
measure_theory.measure.haar_measure_pos_of_is_open
{G : Type u_1}
[group G]
[topological_space G]
[t2_space G]
[topological_group G]
[S : measurable_space G]
[borel_space G]
[locally_compact_space G]
{K₀ : topological_space.positive_compacts G}
{U : set G} :
is_open U → U.nonempty → 0 < ⇑(measure_theory.measure.haar_measure K₀) U
theorem
measure_theory.measure.regular_haar_measure
{G : Type u_1}
[group G]
[topological_space G]
[t2_space G]
[topological_group G]
[S : measurable_space G]
[borel_space G]
[locally_compact_space G]
{K₀ : topological_space.positive_compacts G} :