# Haar measure #

In this file we prove the existence of Haar measure for a locally compact Hausdorff topological group.

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 (`haarMeasure`). We normalize the Haar measure so that the measure of `K₀` is `1`.

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.

We also give a form of uniqueness of Haar measure, for σ-finite measures on second-countable locally compact groups. For more involved statements not assuming second-countability, see the file `Mathlib/MeasureTheory/Measure/Haar/Unique.lean`.

## Main Declarations #

- `haarMeasure`: 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.
- `haarMeasure_self`: the Haar measure is normalized.
- `isMulLeftInvariant_haarMeasure`: the Haar measure is left invariant.
- `regular_haarMeasure`: the Haar measure is a regular measure.
- `isHaarMeasure_haarMeasure`: the Haar measure satisfies the `IsHaarMeasure` typeclass, i.e., it is invariant and gives finite mass to compact sets and positive mass to nonempty open sets.
- `haar` : some choice of a Haar measure, on a locally compact Hausdorff group, constructed as `haarMeasure K` where `K` is some arbitrary choice of a compact set with nonempty interior.
- `haarMeasure_unique`: Every σ-finite left invariant measure on a second-countable locally compact Hausdorff group is a scalar multiple of the Haar 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.
- 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).

source
noncomputable def MeasureTheory.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

- MeasureTheory.Measure.haar.index K V = sInf (Finset.card '' {t : Finset G | K ⊆ ⋃ g ∈ t, (fun (h : G) => g * h) ⁻¹' V})

Instances For

source
noncomputable def MeasureTheory.Measure.haar.addIndex {G : Type u_1} [AddGroup G] (K V : Set G) :
ℕ

additive version of `MeasureTheory.Measure.haar.index`

Equations

- MeasureTheory.Measure.haar.addIndex K V = sInf (Finset.card '' {t : Finset G | K ⊆ ⋃ g ∈ t, (fun (h : G) => g + h) ⁻¹' V})

Instances For

source
theorem MeasureTheory.Measure.haar.index_empty {G : Type u_1} [Group G] {V : Set G} :
index ∅ V = 0
source
theorem MeasureTheory.Measure.haar.addIndex_empty {G : Type u_1} [AddGroup G] {V : Set G} :
addIndex ∅ V = 0
source
noncomputable def MeasureTheory.Measure.haar.prehaar {G : Type u_1} [Group G] [TopologicalSpace G] (K₀ U : Set G) (K : TopologicalSpace.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 `haarProduct` (below).

Equations

- MeasureTheory.Measure.haar.prehaar K₀ U K = ↑(MeasureTheory.Measure.haar.index (↑K) U) / ↑(MeasureTheory.Measure.haar.index K₀ U)

Instances For

source
noncomputable def MeasureTheory.Measure.haar.addPrehaar {G : Type u_1} [AddGroup G] [TopologicalSpace G] (K₀ U : Set G) (K : TopologicalSpace.Compacts G) :
ℝ

additive version of `MeasureTheory.Measure.haar.prehaar`

Equations

- MeasureTheory.Measure.haar.addPrehaar K₀ U K = ↑(MeasureTheory.Measure.haar.addIndex (↑K) U) / ↑(MeasureTheory.Measure.haar.addIndex K₀ U)

Instances For

source
theorem MeasureTheory.Measure.haar.prehaar_empty {G : Type u_1} [Group G] [TopologicalSpace G] (K₀ : TopologicalSpace.PositiveCompacts G) {U : Set G} :
prehaar (↑K₀) U ⊥ = 0
source
theorem MeasureTheory.Measure.haar.addPrehaar_empty {G : Type u_1} [AddGroup G] [TopologicalSpace G] (K₀ : TopologicalSpace.PositiveCompacts G) {U : Set G} :
addPrehaar (↑K₀) U ⊥ = 0
source
theorem MeasureTheory.Measure.haar.prehaar_nonneg {G : Type u_1} [Group G] [TopologicalSpace G] (K₀ : TopologicalSpace.PositiveCompacts G) {U : Set G} (K : TopologicalSpace.Compacts G) :
0 ≤ prehaar (↑K₀) U K
source
theorem MeasureTheory.Measure.haar.addPrehaar_nonneg {G : Type u_1} [AddGroup G] [TopologicalSpace G] (K₀ : TopologicalSpace.PositiveCompacts G) {U : Set G} (K : TopologicalSpace.Compacts G) :
0 ≤ addPrehaar (↑K₀) U K
source
def MeasureTheory.Measure.haar.haarProduct {G : Type u_1} [Group G] [TopologicalSpace G] (K₀ : Set G) :
Set (TopologicalSpace.Compacts G → ℝ)

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

Equations

- MeasureTheory.Measure.haar.haarProduct K₀ = Set.univ.pi fun (K : TopologicalSpace.Compacts G) => Set.Icc 0 ↑(MeasureTheory.Measure.haar.index (↑K) K₀)

Instances For

source
def MeasureTheory.Measure.haar.addHaarProduct {G : Type u_1} [AddGroup G] [TopologicalSpace G] (K₀ : Set G) :
Set (TopologicalSpace.Compacts G → ℝ)

additive version of `MeasureTheory.Measure.haar.haarProduct`

Equations

- MeasureTheory.Measure.haar.addHaarProduct K₀ = Set.univ.pi fun (K : TopologicalSpace.Compacts G) => Set.Icc 0 ↑(MeasureTheory.Measure.haar.addIndex (↑K) K₀)

Instances For

source
@[simp]
theorem MeasureTheory.Measure.haar.mem_prehaar_empty {G : Type u_1} [Group G] [TopologicalSpace G] {K₀ : Set G} {f : TopologicalSpace.Compacts G → ℝ} :
f ∈ haarProduct K₀ ↔ ∀ (K : TopologicalSpace.Compacts G), f K ∈ Set.Icc 0 ↑(index (↑K) K₀)
source
@[simp]
theorem MeasureTheory.Measure.haar.mem_addPrehaar_empty {G : Type u_1} [AddGroup G] [TopologicalSpace G] {K₀ : Set G} {f : TopologicalSpace.Compacts G → ℝ} :
f ∈ addHaarProduct K₀ ↔ ∀ (K : TopologicalSpace.Compacts G), f K ∈ Set.Icc 0 ↑(addIndex (↑K) K₀)
source
def MeasureTheory.Measure.haar.clPrehaar {G : Type u_1} [Group G] [TopologicalSpace G] (K₀ : Set G) (V : TopologicalSpace.OpenNhdsOf 1) :
Set (TopologicalSpace.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.

Equations

- MeasureTheory.Measure.haar.clPrehaar K₀ V = closure (MeasureTheory.Measure.haar.prehaar K₀ '' {U : Set G | U ⊆ ↑V.toOpens ∧ IsOpen U ∧ 1 ∈ U})

Instances For

source
def MeasureTheory.Measure.haar.clAddPrehaar {G : Type u_1} [AddGroup G] [TopologicalSpace G] (K₀ : Set G) (V : TopologicalSpace.OpenNhdsOf 0) :
Set (TopologicalSpace.Compacts G → ℝ)

additive version of `MeasureTheory.Measure.haar.clPrehaar`

Equations

- MeasureTheory.Measure.haar.clAddPrehaar K₀ V = closure (MeasureTheory.Measure.haar.addPrehaar K₀ '' {U : Set G | U ⊆ ↑V.toOpens ∧ IsOpen U ∧ 0 ∈ U})

Instances For

### Lemmas about `index` #

source
theorem MeasureTheory.Measure.haar.index_defined {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {K V : Set G} (hK : IsCompact K) (hV : (interior V).Nonempty) :
∃ (n : ℕ), n ∈ Finset.card '' {t : Finset G | K ⊆ ⋃ g ∈ t, (fun (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.

source
theorem MeasureTheory.Measure.haar.addIndex_defined {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] {K V : Set G} (hK : IsCompact K) (hV : (interior V).Nonempty) :
∃ (n : ℕ), n ∈ Finset.card '' {t : Finset G | K ⊆ ⋃ g ∈ t, (fun (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.

source
theorem MeasureTheory.Measure.haar.index_elim {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {K V : Set G} (hK : IsCompact K) (hV : (interior V).Nonempty) :
∃ (t : Finset G), K ⊆ ⋃ g ∈ t, (fun (h : G) => g * h) ⁻¹' V ∧ t.card = index K V
source
theorem MeasureTheory.Measure.haar.addIndex_elim {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] {K V : Set G} (hK : IsCompact K) (hV : (interior V).Nonempty) :
∃ (t : Finset G), K ⊆ ⋃ g ∈ t, (fun (h : G) => g + h) ⁻¹' V ∧ t.card = addIndex K V
source
theorem MeasureTheory.Measure.haar.le_index_mul {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) (K : TopologicalSpace.Compacts G) {V : Set G} (hV : (interior V).Nonempty) :
index (↑K) V ≤ index ↑K ↑K₀ * index (↑K₀) V
source
theorem MeasureTheory.Measure.haar.le_addIndex_mul {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) (K : TopologicalSpace.Compacts G) {V : Set G} (hV : (interior V).Nonempty) :
addIndex (↑K) V ≤ addIndex ↑K ↑K₀ * addIndex (↑K₀) V
source
theorem MeasureTheory.Measure.haar.index_pos {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (K : TopologicalSpace.PositiveCompacts G) {V : Set G} (hV : (interior V).Nonempty) :
0 < index (↑K) V
source
theorem MeasureTheory.Measure.haar.addIndex_pos {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (K : TopologicalSpace.PositiveCompacts G) {V : Set G} (hV : (interior V).Nonempty) :
0 < addIndex (↑K) V
source
theorem MeasureTheory.Measure.haar.index_mono {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {K K' V : Set G} (hK' : IsCompact K') (h : K ⊆ K') (hV : (interior V).Nonempty) :
index K V ≤ index K' V
source
theorem MeasureTheory.Measure.haar.addIndex_mono {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] {K K' V : Set G} (hK' : IsCompact K') (h : K ⊆ K') (hV : (interior V).Nonempty) :
addIndex K V ≤ addIndex K' V
source
theorem MeasureTheory.Measure.haar.index_union_le {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (K₁ K₂ : TopologicalSpace.Compacts G) {V : Set G} (hV : (interior V).Nonempty) :
index (K₁.carrier ∪ K₂.carrier) V ≤ index K₁.carrier V + index K₂.carrier V
source
theorem MeasureTheory.Measure.haar.addIndex_union_le {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (K₁ K₂ : TopologicalSpace.Compacts G) {V : Set G} (hV : (interior V).Nonempty) :
addIndex (K₁.carrier ∪ K₂.carrier) V ≤ addIndex K₁.carrier V + addIndex K₂.carrier V
source
theorem MeasureTheory.Measure.haar.index_union_eq {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (K₁ K₂ : TopologicalSpace.Compacts G) {V : Set G} (hV : (interior V).Nonempty) (h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)) :
index (K₁.carrier ∪ K₂.carrier) V = index K₁.carrier V + index K₂.carrier V
source
theorem MeasureTheory.Measure.haar.addIndex_union_eq {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (K₁ K₂ : TopologicalSpace.Compacts G) {V : Set G} (hV : (interior V).Nonempty) (h : Disjoint (K₁.carrier + -V) (K₂.carrier + -V)) :
addIndex (K₁.carrier ∪ K₂.carrier) V = addIndex K₁.carrier V + addIndex K₂.carrier V
source
theorem MeasureTheory.Measure.haar.mul_left_index_le {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {K : Set G} (hK : IsCompact K) {V : Set G} (hV : (interior V).Nonempty) (g : G) :
index ((fun (h : G) => g * h) '' K) V ≤ index K V
source
theorem MeasureTheory.Measure.haar.add_left_addIndex_le {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] {K : Set G} (hK : IsCompact K) {V : Set G} (hV : (interior V).Nonempty) (g : G) :
addIndex ((fun (h : G) => g + h) '' K) V ≤ addIndex K V
source
theorem MeasureTheory.Measure.haar.is_left_invariant_index {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {K : Set G} (hK : IsCompact K) (g : G) {V : Set G} (hV : (interior V).Nonempty) :
index ((fun (h : G) => g * h) '' K) V = index K V
source
theorem MeasureTheory.Measure.haar.is_left_invariant_addIndex {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] {K : Set G} (hK : IsCompact K) (g : G) {V : Set G} (hV : (interior V).Nonempty) :
addIndex ((fun (h : G) => g + h) '' K) V = addIndex K V

### Lemmas about `prehaar` #

source
theorem MeasureTheory.Measure.haar.prehaar_le_index {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) {U : Set G} (K : TopologicalSpace.Compacts G) (hU : (interior U).Nonempty) :
prehaar (↑K₀) U K ≤ ↑(index ↑K ↑K₀)
source
theorem MeasureTheory.Measure.haar.add_prehaar_le_addIndex {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) {U : Set G} (K : TopologicalSpace.Compacts G) (hU : (interior U).Nonempty) :
addPrehaar (↑K₀) U K ≤ ↑(addIndex ↑K ↑K₀)
source
theorem MeasureTheory.Measure.haar.prehaar_pos {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) {U : Set G} (hU : (interior U).Nonempty) {K : Set G} (h1K : IsCompact K) (h2K : (interior K).Nonempty) :
0 < prehaar (↑K₀) U { carrier := K, isCompact' := h1K }
source
theorem MeasureTheory.Measure.haar.addPrehaar_pos {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) {U : Set G} (hU : (interior U).Nonempty) {K : Set G} (h1K : IsCompact K) (h2K : (interior K).Nonempty) :
0 < addPrehaar (↑K₀) U { carrier := K, isCompact' := h1K }
source
theorem MeasureTheory.Measure.haar.prehaar_mono {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {K₀ : TopologicalSpace.PositiveCompacts G} {U : Set G} (hU : (interior U).Nonempty) {K₁ K₂ : TopologicalSpace.Compacts G} (h : ↑K₁ ⊆ K₂.carrier) :
prehaar (↑K₀) U K₁ ≤ prehaar (↑K₀) U K₂
source
theorem MeasureTheory.Measure.haar.addPrehaar_mono {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] {K₀ : TopologicalSpace.PositiveCompacts G} {U : Set G} (hU : (interior U).Nonempty) {K₁ K₂ : TopologicalSpace.Compacts G} (h : ↑K₁ ⊆ K₂.carrier) :
addPrehaar (↑K₀) U K₁ ≤ addPrehaar (↑K₀) U K₂
source
theorem MeasureTheory.Measure.haar.prehaar_self {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {K₀ : TopologicalSpace.PositiveCompacts G} {U : Set G} (hU : (interior U).Nonempty) :
prehaar (↑K₀) U K₀.toCompacts = 1
source
theorem MeasureTheory.Measure.haar.addPrehaar_self {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] {K₀ : TopologicalSpace.PositiveCompacts G} {U : Set G} (hU : (interior U).Nonempty) :
addPrehaar (↑K₀) U K₀.toCompacts = 1
source
theorem MeasureTheory.Measure.haar.prehaar_sup_le {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {K₀ : TopologicalSpace.PositiveCompacts G} {U : Set G} (K₁ K₂ : TopologicalSpace.Compacts G) (hU : (interior U).Nonempty) :
prehaar (↑K₀) U (K₁ ⊔ K₂) ≤ prehaar (↑K₀) U K₁ + prehaar (↑K₀) U K₂
source
theorem MeasureTheory.Measure.haar.addPrehaar_sup_le {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] {K₀ : TopologicalSpace.PositiveCompacts G} {U : Set G} (K₁ K₂ : TopologicalSpace.Compacts G) (hU : (interior U).Nonempty) :
addPrehaar (↑K₀) U (K₁ ⊔ K₂) ≤ addPrehaar (↑K₀) U K₁ + addPrehaar (↑K₀) U K₂
source
theorem MeasureTheory.Measure.haar.prehaar_sup_eq {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {K₀ : TopologicalSpace.PositiveCompacts G} {U : Set G} {K₁ K₂ : TopologicalSpace.Compacts G} (hU : (interior U).Nonempty) (h : Disjoint (K₁.carrier * U⁻¹) (K₂.carrier * U⁻¹)) :
prehaar (↑K₀) U (K₁ ⊔ K₂) = prehaar (↑K₀) U K₁ + prehaar (↑K₀) U K₂
source
theorem MeasureTheory.Measure.haar.addPrehaar_sup_eq {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] {K₀ : TopologicalSpace.PositiveCompacts G} {U : Set G} {K₁ K₂ : TopologicalSpace.Compacts G} (hU : (interior U).Nonempty) (h : Disjoint (K₁.carrier + -U) (K₂.carrier + -U)) :
addPrehaar (↑K₀) U (K₁ ⊔ K₂) = addPrehaar (↑K₀) U K₁ + addPrehaar (↑K₀) U K₂
source
theorem MeasureTheory.Measure.haar.is_left_invariant_prehaar {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {K₀ : TopologicalSpace.PositiveCompacts G} {U : Set G} (hU : (interior U).Nonempty) (g : G) (K : TopologicalSpace.Compacts G) :
prehaar (↑K₀) U (TopologicalSpace.Compacts.map (fun (b : G) => g * b) ⋯ K) = prehaar (↑K₀) U K
source
theorem MeasureTheory.Measure.haar.is_left_invariant_addPrehaar {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] {K₀ : TopologicalSpace.PositiveCompacts G} {U : Set G} (hU : (interior U).Nonempty) (g : G) (K : TopologicalSpace.Compacts G) :
addPrehaar (↑K₀) U (TopologicalSpace.Compacts.map (fun (b : G) => g + b) ⋯ K) = addPrehaar (↑K₀) U K

### Lemmas about `haarProduct` #

source
theorem MeasureTheory.Measure.haar.prehaar_mem_haarProduct {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) {U : Set G} (hU : (interior U).Nonempty) :
prehaar (↑K₀) U ∈ haarProduct ↑K₀
source
theorem MeasureTheory.Measure.haar.addPrehaar_mem_addHaarProduct {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) {U : Set G} (hU : (interior U).Nonempty) :
addPrehaar (↑K₀) U ∈ addHaarProduct ↑K₀
source
theorem MeasureTheory.Measure.haar.nonempty_iInter_clPrehaar {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) :
(haarProduct ↑K₀ ∩ ⋂ (V : TopologicalSpace.OpenNhdsOf 1), clPrehaar (↑K₀) V).Nonempty
source
theorem MeasureTheory.Measure.haar.nonempty_iInter_clAddPrehaar {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) :
(addHaarProduct ↑K₀ ∩ ⋂ (V : TopologicalSpace.OpenNhdsOf 0), clAddPrehaar (↑K₀) V).Nonempty

### Lemmas about `chaar` #

source
noncomputable def MeasureTheory.Measure.haar.chaar {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) (K : TopologicalSpace.Compacts G) :
ℝ

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 `clPrehaar K₀ V` in `haarProduct K₀`. This is roughly equal to the Haar measure on compact sets, but it can differ slightly. We do know that `haarMeasure K₀ (interior K) ≤ chaar K₀ K ≤ haarMeasure K₀ K`.

Equations

- MeasureTheory.Measure.haar.chaar K₀ K = Classical.choose ⋯ K

Instances For

source
noncomputable def MeasureTheory.Measure.haar.addCHaar {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) (K : TopologicalSpace.Compacts G) :
ℝ

additive version of `MeasureTheory.Measure.haar.chaar`

Equations

- MeasureTheory.Measure.haar.addCHaar K₀ K = Classical.choose ⋯ K

Instances For

source
theorem MeasureTheory.Measure.haar.chaar_mem_haarProduct {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) :
chaar K₀ ∈ haarProduct ↑K₀
source
theorem MeasureTheory.Measure.haar.addCHaar_mem_addHaarProduct {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) :
addCHaar K₀ ∈ addHaarProduct ↑K₀
source
theorem MeasureTheory.Measure.haar.chaar_mem_clPrehaar {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) (V : TopologicalSpace.OpenNhdsOf 1) :
chaar K₀ ∈ clPrehaar (↑K₀) V
source
theorem MeasureTheory.Measure.haar.addCHaar_mem_clAddPrehaar {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) (V : TopologicalSpace.OpenNhdsOf 0) :
addCHaar K₀ ∈ clAddPrehaar (↑K₀) V
source
theorem MeasureTheory.Measure.haar.chaar_nonneg {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) (K : TopologicalSpace.Compacts G) :
0 ≤ chaar K₀ K
source
theorem MeasureTheory.Measure.haar.addCHaar_nonneg {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) (K : TopologicalSpace.Compacts G) :
0 ≤ addCHaar K₀ K
source
theorem MeasureTheory.Measure.haar.chaar_empty {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) :
chaar K₀ ⊥ = 0
source
theorem MeasureTheory.Measure.haar.addCHaar_empty {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) :
addCHaar K₀ ⊥ = 0
source
theorem MeasureTheory.Measure.haar.chaar_self {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) :
chaar K₀ K₀.toCompacts = 1
source
theorem MeasureTheory.Measure.haar.addCHaar_self {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) :
addCHaar K₀ K₀.toCompacts = 1
source
theorem MeasureTheory.Measure.haar.chaar_mono {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {K₀ : TopologicalSpace.PositiveCompacts G} {K₁ K₂ : TopologicalSpace.Compacts G} (h : ↑K₁ ⊆ ↑K₂) :
chaar K₀ K₁ ≤ chaar K₀ K₂
source
theorem MeasureTheory.Measure.haar.addCHaar_mono {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] {K₀ : TopologicalSpace.PositiveCompacts G} {K₁ K₂ : TopologicalSpace.Compacts G} (h : ↑K₁ ⊆ ↑K₂) :
addCHaar K₀ K₁ ≤ addCHaar K₀ K₂
source
theorem MeasureTheory.Measure.haar.chaar_sup_le {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {K₀ : TopologicalSpace.PositiveCompacts G} (K₁ K₂ : TopologicalSpace.Compacts G) :
chaar K₀ (K₁ ⊔ K₂) ≤ chaar K₀ K₁ + chaar K₀ K₂
source
theorem MeasureTheory.Measure.haar.addCHaar_sup_le {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] {K₀ : TopologicalSpace.PositiveCompacts G} (K₁ K₂ : TopologicalSpace.Compacts G) :
addCHaar K₀ (K₁ ⊔ K₂) ≤ addCHaar K₀ K₁ + addCHaar K₀ K₂
source
theorem MeasureTheory.Measure.haar.chaar_sup_eq {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {K₀ : TopologicalSpace.PositiveCompacts G} {K₁ K₂ : TopologicalSpace.Compacts G} (h : Disjoint K₁.carrier K₂.carrier) (h₂ : IsClosed K₂.carrier) :
chaar K₀ (K₁ ⊔ K₂) = chaar K₀ K₁ + chaar K₀ K₂
source
theorem MeasureTheory.Measure.haar.addCHaar_sup_eq {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] {K₀ : TopologicalSpace.PositiveCompacts G} {K₁ K₂ : TopologicalSpace.Compacts G} (h : Disjoint K₁.carrier K₂.carrier) (h₂ : IsClosed K₂.carrier) :
addCHaar K₀ (K₁ ⊔ K₂) = addCHaar K₀ K₁ + addCHaar K₀ K₂
source
theorem MeasureTheory.Measure.haar.is_left_invariant_chaar {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {K₀ : TopologicalSpace.PositiveCompacts G} (g : G) (K : TopologicalSpace.Compacts G) :
chaar K₀ (TopologicalSpace.Compacts.map (fun (b : G) => g * b) ⋯ K) = chaar K₀ K
source
theorem MeasureTheory.Measure.haar.is_left_invariant_addCHaar {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] {K₀ : TopologicalSpace.PositiveCompacts G} (g : G) (K : TopologicalSpace.Compacts G) :
addCHaar K₀ (TopologicalSpace.Compacts.map (fun (b : G) => g + b) ⋯ K) = addCHaar K₀ K
source
noncomputable def MeasureTheory.Measure.haar.haarContent {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) :
Content G

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

Equations

- MeasureTheory.Measure.haar.haarContent K₀ = { toFun := fun (K : TopologicalSpace.Compacts G) => ⟨MeasureTheory.Measure.haar.chaar K₀ K, ⋯⟩, mono' := ⋯, sup_disjoint' := ⋯, sup_le' := ⋯ }

Instances For

source
noncomputable def MeasureTheory.Measure.haar.addHaarContent {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) :
Content G

additive version of `MeasureTheory.Measure.haar.haarContent`

Equations

- MeasureTheory.Measure.haar.addHaarContent K₀ = { toFun := fun (K : TopologicalSpace.Compacts G) => ⟨MeasureTheory.Measure.haar.addCHaar K₀ K, ⋯⟩, mono' := ⋯, sup_disjoint' := ⋯, sup_le' := ⋯ }

Instances For

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

source
theorem MeasureTheory.Measure.haar.haarContent_apply {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) (K : TopologicalSpace.Compacts G) :
(haarContent K₀) K = ↑(have this := ⟨chaar K₀ K, ⋯⟩; this)
source
theorem MeasureTheory.Measure.haar.addHaarContent_apply {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) (K : TopologicalSpace.Compacts G) :
(addHaarContent K₀) K = ↑(have this := ⟨addCHaar K₀ K, ⋯⟩; this)
source
theorem MeasureTheory.Measure.haar.haarContent_self {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {K₀ : TopologicalSpace.PositiveCompacts G} :
(haarContent K₀) K₀.toCompacts = 1

The variant of `chaar_self` for `haarContent`

source
theorem MeasureTheory.Measure.haar.addHaarContent_self {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] {K₀ : TopologicalSpace.PositiveCompacts G} :
(addHaarContent K₀) K₀.toCompacts = 1

The variant of `addCHaar_self` for `addHaarContent`.

source
theorem MeasureTheory.Measure.haar.is_left_invariant_haarContent {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {K₀ : TopologicalSpace.PositiveCompacts G} (g : G) (K : TopologicalSpace.Compacts G) :
(haarContent K₀) (TopologicalSpace.Compacts.map (fun (b : G) => g * b) ⋯ K) = (haarContent K₀) K

The variant of `is_left_invariant_chaar` for `haarContent`

source
theorem MeasureTheory.Measure.haar.is_left_invariant_addHaarContent {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] {K₀ : TopologicalSpace.PositiveCompacts G} (g : G) (K : TopologicalSpace.Compacts G) :
(addHaarContent K₀) (TopologicalSpace.Compacts.map (fun (b : G) => g + b) ⋯ K) = (addHaarContent K₀) K

The variant of `is_left_invariant_addCHaar` for `addHaarContent`

source
theorem MeasureTheory.Measure.haar.haarContent_outerMeasure_self_pos {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) :
0 < (haarContent K₀).outerMeasure ↑K₀
source
theorem MeasureTheory.Measure.haar.addHaarContent_outerMeasure_self_pos {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) :
0 < (addHaarContent K₀).outerMeasure ↑K₀
source
theorem MeasureTheory.Measure.haar.haarContent_outerMeasure_closure_pos {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) :
0 < (haarContent K₀).outerMeasure (closure ↑K₀)
source
theorem MeasureTheory.Measure.haar.addHaarContent_outerMeasure_closure_pos {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) :
0 < (addHaarContent K₀).outerMeasure (closure ↑K₀)

### The Haar measure #

source
noncomputable def MeasureTheory.Measure.haarMeasure {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [MeasurableSpace G] [BorelSpace G] (K₀ : TopologicalSpace.PositiveCompacts G) :
Measure G

The Haar measure on the locally compact group `G`, scaled so that `haarMeasure K₀ K₀ = 1`.

Equations

- MeasureTheory.Measure.haarMeasure K₀ = ((MeasureTheory.Measure.haar.haarContent K₀).measure ↑K₀)⁻¹ • (MeasureTheory.Measure.haar.haarContent K₀).measure

Instances For

source
noncomputable def MeasureTheory.Measure.addHaarMeasure {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] (K₀ : TopologicalSpace.PositiveCompacts G) :
Measure G

The Haar measure on the locally compact additive group `G`, scaled so that `addHaarMeasure K₀ K₀ = 1`.

Equations

- MeasureTheory.Measure.addHaarMeasure K₀ = ((MeasureTheory.Measure.haar.addHaarContent K₀).measure ↑K₀)⁻¹ • (MeasureTheory.Measure.haar.addHaarContent K₀).measure

Instances For

source
theorem MeasureTheory.Measure.haarMeasure_apply {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [MeasurableSpace G] [BorelSpace G] {K₀ : TopologicalSpace.PositiveCompacts G} {s : Set G} (hs : MeasurableSet s) :
(haarMeasure K₀) s = (haar.haarContent K₀).outerMeasure s / (haar.haarContent K₀).measure ↑K₀
source
theorem MeasureTheory.Measure.addHaarMeasure_apply {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] {K₀ : TopologicalSpace.PositiveCompacts G} {s : Set G} (hs : MeasurableSet s) :
(addHaarMeasure K₀) s = (haar.addHaarContent K₀).outerMeasure s / (haar.addHaarContent K₀).measure ↑K₀
source
instance MeasureTheory.Measure.isMulLeftInvariant_haarMeasure {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [MeasurableSpace G] [BorelSpace G] (K₀ : TopologicalSpace.PositiveCompacts G) :
(haarMeasure K₀).IsMulLeftInvariant
source
instance MeasureTheory.Measure.isAddLeftInvariant_addHaarMeasure {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] (K₀ : TopologicalSpace.PositiveCompacts G) :
(addHaarMeasure K₀).IsAddLeftInvariant
source
theorem MeasureTheory.Measure.haarMeasure_self {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [MeasurableSpace G] [BorelSpace G] {K₀ : TopologicalSpace.PositiveCompacts G} :
(haarMeasure K₀) ↑K₀ = 1
source
theorem MeasureTheory.Measure.addHaarMeasure_self {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] {K₀ : TopologicalSpace.PositiveCompacts G} :
(addHaarMeasure K₀) ↑K₀ = 1
source
instance MeasureTheory.Measure.regular_haarMeasure {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [MeasurableSpace G] [BorelSpace G] {K₀ : TopologicalSpace.PositiveCompacts G} :
(haarMeasure K₀).Regular

The Haar measure is regular.

source
instance MeasureTheory.Measure.regular_addHaarMeasure {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] {K₀ : TopologicalSpace.PositiveCompacts G} :
(addHaarMeasure K₀).Regular

The additive Haar measure is regular.

source
theorem MeasureTheory.Measure.haarMeasure_closure_self {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [MeasurableSpace G] [BorelSpace G] {K₀ : TopologicalSpace.PositiveCompacts G} :
(haarMeasure K₀) (closure ↑K₀) = 1
source
theorem MeasureTheory.Measure.addHaarMeasure_closure_self {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] {K₀ : TopologicalSpace.PositiveCompacts G} :
(addHaarMeasure K₀) (closure ↑K₀) = 1
source
instance MeasureTheory.Measure.sigmaFinite_haarMeasure {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [MeasurableSpace G] [BorelSpace G] [SecondCountableTopology G] {K₀ : TopologicalSpace.PositiveCompacts G} :
SigmaFinite (haarMeasure K₀)

The Haar measure is sigma-finite in a second countable group.

source
instance MeasureTheory.Measure.sigmaFinite_addHaarMeasure {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] [SecondCountableTopology G] {K₀ : TopologicalSpace.PositiveCompacts G} :
SigmaFinite (addHaarMeasure K₀)

The additive Haar measure is sigma-finite in a second countable group.

source
instance MeasureTheory.Measure.isHaarMeasure_haarMeasure {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [MeasurableSpace G] [BorelSpace G] (K₀ : TopologicalSpace.PositiveCompacts G) :
(haarMeasure K₀).IsHaarMeasure

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.

source
instance MeasureTheory.Measure.isAddHaarMeasure_addHaarMeasure {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] (K₀ : TopologicalSpace.PositiveCompacts G) :
(addHaarMeasure K₀).IsAddHaarMeasure

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.

source
@[reducible, inline]
noncomputable abbrev MeasureTheory.Measure.haar {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [MeasurableSpace G] [BorelSpace G] [LocallyCompactSpace G] :
Measure G

`haar` is some choice of a Haar measure, on a locally compact group.

Equations

- MeasureTheory.Measure.haar = MeasureTheory.Measure.haarMeasure (Classical.arbitrary (TopologicalSpace.PositiveCompacts G))

Instances For

source
@[reducible, inline]
noncomputable abbrev MeasureTheory.Measure.addHaar {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] [LocallyCompactSpace G] :
Measure G

`addHaar` is some choice of a Haar measure, on a locally compact additive group.

Equations

- MeasureTheory.Measure.addHaar = MeasureTheory.Measure.addHaarMeasure (Classical.arbitrary (TopologicalSpace.PositiveCompacts G))

Instances For

Steinhaus theorem: if `E` has positive measure, then `E / E` contains a neighborhood of zero. Note that this is not true for general regular Haar measures: in `ℝ × ℝ` where the first factor has the discrete topology, then `E = ℝ × {0}` has infinite measure for the regular Haar measure, but `E / E` does not contain a neighborhood of zero. On the other hand, it is always true for inner regular Haar measures (and in particular for any Haar measure on a second countable group).

source
theorem MeasureTheory.Measure.div_mem_nhds_one_of_haar_pos_ne_top {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [MeasurableSpace G] [BorelSpace G] (μ : Measure G) [μ.IsHaarMeasure] [LocallyCompactSpace G] [μ.InnerRegularCompactLTTop] (E : Set G) (hE : MeasurableSet E) (hEpos : 0 < μ E) (hEfin : μ E ≠ ⊤) :
E / E ∈ nhds 1

Steinhaus Theorem for finite mass sets.

In any locally compact group `G` with an Haar measure `μ` that's inner regular on finite measure sets, for any measurable set `E` of finite positive measure, the set `E / E` is a neighbourhood of `1`.

source
theorem MeasureTheory.Measure.sub_mem_nhds_zero_of_addHaar_pos_ne_top {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] (μ : Measure G) [μ.IsAddHaarMeasure] [LocallyCompactSpace G] [μ.InnerRegularCompactLTTop] (E : Set G) (hE : MeasurableSet E) (hEpos : 0 < μ E) (hEfin : μ E ≠ ⊤) :
E - E ∈ nhds 0

Steinhaus Theorem for finite mass sets.

In any locally compact group `G` with an Haar measure `μ` that's inner regular on finite measure sets, for any measurable set `E` of finite positive measure, the set `E - E` is a neighbourhood of `0`.

source
theorem MeasureTheory.Measure.div_mem_nhds_one_of_haar_pos {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [MeasurableSpace G] [BorelSpace G] (μ : Measure G) [μ.IsHaarMeasure] [LocallyCompactSpace G] [μ.InnerRegular] (E : Set G) (hE : MeasurableSet E) (hEpos : 0 < μ E) :
E / E ∈ nhds 1

Steinhaus Theorem.

In any locally compact group `G` with an inner regular Haar measure `μ`, for any measurable set `E` of positive measure, the set `E / E` is a neighbourhood of `1`.

source
theorem MeasureTheory.Measure.sub_mem_nhds_zero_of_addHaar_pos {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] (μ : Measure G) [μ.IsAddHaarMeasure] [LocallyCompactSpace G] [μ.InnerRegular] (E : Set G) (hE : MeasurableSet E) (hEpos : 0 < μ E) :
E - E ∈ nhds 0

Steinhaus Theorem.

In any locally compact group `G` with an inner regular Haar measure `μ`, for any measurable set `E` of positive measure, the set `E - E` is a neighbourhood of `0`.

In this section, we investigate uniqueness of left-invariant measures without assuming that the measure is finite on compact sets, but assuming σ-finiteness instead. We also rely on second-countability, to ensure that the group operations are measurable: in this case, one can bypass all topological arguments, and conclude using uniqueness of σ-finite left-invariant measures in measurable groups.

For more general uniqueness statements without second-countability assumptions, see the file `Mathlib/MeasureTheory/Measure/Haar/Unique.lean`.

source
theorem MeasureTheory.Measure.haarMeasure_unique {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [MeasurableSpace G] [BorelSpace G] [SecondCountableTopology G] (μ : Measure G) [SigmaFinite μ] [μ.IsMulLeftInvariant] (K₀ : TopologicalSpace.PositiveCompacts G) :
μ = μ ↑K₀ • haarMeasure K₀

Uniqueness of left-invariant measures: In a second-countable locally compact group, any σ-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`). See also `isMulLeftInvariant_eq_smul_of_regular` for a statement not assuming second-countability.

source
theorem MeasureTheory.Measure.addHaarMeasure_unique {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] [SecondCountableTopology G] (μ : Measure G) [SigmaFinite μ] [μ.IsAddLeftInvariant] (K₀ : TopologicalSpace.PositiveCompacts G) :
μ = μ ↑K₀ • addHaarMeasure K₀

Uniqueness of left-invariant measures: In a second-countable locally compact additive group, any σ-finite left-invariant measure is a scalar multiple of the additive Haar measure. This is slightly weaker than assuming that `μ` is a additive Haar measure (in particular we don't require `μ ≠ 0`). See also `isAddLeftInvariant_eq_smul_of_regular` for a statement not assuming second-countability.

source
theorem MeasureTheory.Measure.haarMeasure_eq_iff {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [MeasurableSpace G] [BorelSpace G] [SecondCountableTopology G] (K₀ : TopologicalSpace.PositiveCompacts G) (μ : Measure G) [SigmaFinite μ] [μ.IsMulLeftInvariant] :
haarMeasure K₀ = μ ↔ μ ↑K₀ = 1

Let `μ` be a σ-finite left invariant measure on `G`. Then `μ` is equal to the Haar measure defined by `K₀` iff `μ K₀ = 1`.

source
theorem MeasureTheory.Measure.addHaarMeasure_eq_iff {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] [SecondCountableTopology G] (K₀ : TopologicalSpace.PositiveCompacts G) (μ : Measure G) [SigmaFinite μ] [μ.IsAddLeftInvariant] :
addHaarMeasure K₀ = μ ↔ μ ↑K₀ = 1
source
theorem MeasureTheory.Measure.regular_of_isMulLeftInvariant {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [MeasurableSpace G] [BorelSpace G] [SecondCountableTopology G] {μ : Measure G} [SigmaFinite μ] [μ.IsMulLeftInvariant] {K : Set G} (hK : IsCompact K) (h2K : (interior K).Nonempty) (hμK : μ K ≠ ⊤) :
μ.Regular

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.

source
theorem MeasureTheory.Measure.regular_of_isAddLeftInvariant {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] [SecondCountableTopology G] {μ : Measure G} [SigmaFinite μ] [μ.IsAddLeftInvariant] {K : Set G} (hK : IsCompact K) (h2K : (interior K).Nonempty) (hμK : μ K ≠ ⊤) :
μ.Regular

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.