Haar measure

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

• 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 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).

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

additive version of MeasureTheory.Measure.haar.index

noncomputable def MeasureTheory.Measure.haar.index {G : Type u_1} [Group G] (K : Set G) (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.

theorem MeasureTheory.Measure.haar.addIndex_empty {G : Type u_1} [AddGroup G] {V : Set G} : MeasureTheory.Measure.haar.addIndex ∅ V = 0

theorem MeasureTheory.Measure.haar.index_empty {G : Type u_1} [Group G] {V : Set G} : MeasureTheory.Measure.haar.index ∅ V = 0

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

additive version of MeasureTheory.Measure.haar.prehaar

noncomputable def MeasureTheory.Measure.haar.prehaar {G : Type u_1} [Group G] [TopologicalSpace G] (K₀ : Set G) (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).

theorem MeasureTheory.Measure.haar.addPrehaar_empty {G : Type u_1} [AddGroup G] [TopologicalSpace G] (K₀ : TopologicalSpace.PositiveCompacts G) {U : Set G} : MeasureTheory.Measure.haar.addPrehaar (↑K₀) U ⊥ = 0

theorem MeasureTheory.Measure.haar.prehaar_empty {G : Type u_1} [Group G] [TopologicalSpace G] (K₀ : TopologicalSpace.PositiveCompacts G) {U : Set G} : MeasureTheory.Measure.haar.prehaar (↑K₀) U ⊥ = 0

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 ≤ MeasureTheory.Measure.haar.addPrehaar (↑K₀) U K

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 ≤ MeasureTheory.Measure.haar.prehaar (↑K₀) U K

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

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

@[simp]

theorem MeasureTheory.Measure.haar.mem_addPrehaar_empty {G : Type u_1} [AddGroup G] [TopologicalSpace G] {K₀ : Set G} {f : TopologicalSpace.Compacts G → ℝ} : f ∈ MeasureTheory.Measure.haar.addHaarProduct K₀ ↔ ∀ (K : TopologicalSpace.Compacts G), f K ∈ Set.Icc 0 ↑(MeasureTheory.Measure.haar.addIndex (↑K) K₀)

@[simp]

theorem MeasureTheory.Measure.haar.mem_prehaar_empty {G : Type u_1} [Group G] [TopologicalSpace G] {K₀ : Set G} {f : TopologicalSpace.Compacts G → ℝ} : f ∈ MeasureTheory.Measure.haar.haarProduct K₀ ↔ ∀ (K : TopologicalSpace.Compacts G), f K ∈ Set.Icc 0 ↑(MeasureTheory.Measure.haar.index (↑K) K₀)

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

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.

Lemmas about index

theorem MeasureTheory.Measure.haar.addIndex_defined {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] {K : Set G} {V : Set G} (hK : IsCompact K) (hV : Set.Nonempty (interior V)) : ∃ n, n ∈ Finset.card '' {t | K ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => 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 MeasureTheory.Measure.haar.index_defined {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] {K : Set G} {V : Set G} (hK : IsCompact K) (hV : Set.Nonempty (interior V)) : ∃ n, n ∈ Finset.card '' {t | K ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => 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 MeasureTheory.Measure.haar.addIndex_elim {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] {K : Set G} {V : Set G} (hK : IsCompact K) (hV : Set.Nonempty (interior V)) : ∃ t, K ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g + h) ⁻¹' V ∧ Finset.card t = MeasureTheory.Measure.haar.addIndex K V

theorem MeasureTheory.Measure.haar.index_elim {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] {K : Set G} {V : Set G} (hK : IsCompact K) (hV : Set.Nonempty (interior V)) : ∃ t, K ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V ∧ Finset.card t = MeasureTheory.Measure.haar.index K V

theorem MeasureTheory.Measure.haar.le_addIndex_mul {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) (K : TopologicalSpace.Compacts G) {V : Set G} (hV : Set.Nonempty (interior V)) : MeasureTheory.Measure.haar.addIndex (↑K) V ≤ MeasureTheory.Measure.haar.addIndex ↑K ↑K₀ * MeasureTheory.Measure.haar.addIndex (↑K₀) V

theorem MeasureTheory.Measure.haar.le_index_mul {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) (K : TopologicalSpace.Compacts G) {V : Set G} (hV : Set.Nonempty (interior V)) : MeasureTheory.Measure.haar.index (↑K) V ≤ MeasureTheory.Measure.haar.index ↑K ↑K₀ * MeasureTheory.Measure.haar.index (↑K₀) V

theorem MeasureTheory.Measure.haar.addIndex_pos {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (K : TopologicalSpace.PositiveCompacts G) {V : Set G} (hV : Set.Nonempty (interior V)) : 0 < MeasureTheory.Measure.haar.addIndex (↑K) V

theorem MeasureTheory.Measure.haar.index_pos {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] (K : TopologicalSpace.PositiveCompacts G) {V : Set G} (hV : Set.Nonempty (interior V)) : 0 < MeasureTheory.Measure.haar.index (↑K) V

theorem MeasureTheory.Measure.haar.addIndex_mono {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] {K : Set G} {K' : Set G} {V : Set G} (hK' : IsCompact K') (h : K ⊆ K') (hV : Set.Nonempty (interior V)) : MeasureTheory.Measure.haar.addIndex K V ≤ MeasureTheory.Measure.haar.addIndex K' V

theorem MeasureTheory.Measure.haar.index_mono {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] {K : Set G} {K' : Set G} {V : Set G} (hK' : IsCompact K') (h : K ⊆ K') (hV : Set.Nonempty (interior V)) : MeasureTheory.Measure.haar.index K V ≤ MeasureTheory.Measure.haar.index K' V

theorem MeasureTheory.Measure.haar.addIndex_union_le {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (K₁ : TopologicalSpace.Compacts G) (K₂ : TopologicalSpace.Compacts G) {V : Set G} (hV : Set.Nonempty (interior V)) : MeasureTheory.Measure.haar.addIndex (K₁.carrier ∪ K₂.carrier) V ≤ MeasureTheory.Measure.haar.addIndex K₁.carrier V + MeasureTheory.Measure.haar.addIndex K₂.carrier V

theorem MeasureTheory.Measure.haar.index_union_le {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] (K₁ : TopologicalSpace.Compacts G) (K₂ : TopologicalSpace.Compacts G) {V : Set G} (hV : Set.Nonempty (interior V)) : MeasureTheory.Measure.haar.index (K₁.carrier ∪ K₂.carrier) V ≤ MeasureTheory.Measure.haar.index K₁.carrier V + MeasureTheory.Measure.haar.index K₂.carrier V

theorem MeasureTheory.Measure.haar.addIndex_union_eq {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (K₁ : TopologicalSpace.Compacts G) (K₂ : TopologicalSpace.Compacts G) {V : Set G} (hV : Set.Nonempty (interior V)) (h : Disjoint (K₁.carrier + -V) (K₂.carrier + -V)) : MeasureTheory.Measure.haar.addIndex (K₁.carrier ∪ K₂.carrier) V = MeasureTheory.Measure.haar.addIndex K₁.carrier V + MeasureTheory.Measure.haar.addIndex K₂.carrier V

theorem MeasureTheory.Measure.haar.index_union_eq {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] (K₁ : TopologicalSpace.Compacts G) (K₂ : TopologicalSpace.Compacts G) {V : Set G} (hV : Set.Nonempty (interior V)) (h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)) : MeasureTheory.Measure.haar.index (K₁.carrier ∪ K₂.carrier) V = MeasureTheory.Measure.haar.index K₁.carrier V + MeasureTheory.Measure.haar.index K₂.carrier V

theorem MeasureTheory.Measure.haar.add_left_addIndex_le {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] {K : Set G} (hK : IsCompact K) {V : Set G} (hV : Set.Nonempty (interior V)) (g : G) : MeasureTheory.Measure.haar.addIndex ((fun h => g + h) '' K) V ≤ MeasureTheory.Measure.haar.addIndex K V

theorem MeasureTheory.Measure.haar.mul_left_index_le {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] {K : Set G} (hK : IsCompact K) {V : Set G} (hV : Set.Nonempty (interior V)) (g : G) : MeasureTheory.Measure.haar.index ((fun h => g * h) '' K) V ≤ MeasureTheory.Measure.haar.index K V

theorem MeasureTheory.Measure.haar.is_left_invariant_addIndex {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] {K : Set G} (hK : IsCompact K) (g : G) {V : Set G} (hV : Set.Nonempty (interior V)) : MeasureTheory.Measure.haar.addIndex ((fun h => g + h) '' K) V = MeasureTheory.Measure.haar.addIndex K V

theorem MeasureTheory.Measure.haar.is_left_invariant_index {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] {K : Set G} (hK : IsCompact K) (g : G) {V : Set G} (hV : Set.Nonempty (interior V)) : MeasureTheory.Measure.haar.index ((fun h => g * h) '' K) V = MeasureTheory.Measure.haar.index K V

Lemmas about prehaar

theorem MeasureTheory.Measure.haar.add_prehaar_le_addIndex {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) {U : Set G} (K : TopologicalSpace.Compacts G) (hU : Set.Nonempty (interior U)) : MeasureTheory.Measure.haar.addPrehaar (↑K₀) U K ≤ ↑(MeasureTheory.Measure.haar.addIndex ↑K ↑K₀)

theorem MeasureTheory.Measure.haar.prehaar_le_index {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) {U : Set G} (K : TopologicalSpace.Compacts G) (hU : Set.Nonempty (interior U)) : MeasureTheory.Measure.haar.prehaar (↑K₀) U K ≤ ↑(MeasureTheory.Measure.haar.index ↑K ↑K₀)

theorem MeasureTheory.Measure.haar.addPrehaar_pos {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) {U : Set G} (hU : Set.Nonempty (interior U)) {K : Set G} (h1K : IsCompact K) (h2K : Set.Nonempty (interior K)) : 0 < MeasureTheory.Measure.haar.addPrehaar (↑K₀) U { carrier := K, isCompact' := h1K }

theorem MeasureTheory.Measure.haar.prehaar_pos {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) {U : Set G} (hU : Set.Nonempty (interior U)) {K : Set G} (h1K : IsCompact K) (h2K : Set.Nonempty (interior K)) : 0 < MeasureTheory.Measure.haar.prehaar (↑K₀) U { carrier := K, isCompact' := h1K }

theorem MeasureTheory.Measure.haar.addPrehaar_mono {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] {K₀ : TopologicalSpace.PositiveCompacts G} {U : Set G} (hU : Set.Nonempty (interior U)) {K₁ : TopologicalSpace.Compacts G} {K₂ : TopologicalSpace.Compacts G} (h : ↑K₁ ⊆ K₂.carrier) : MeasureTheory.Measure.haar.addPrehaar (↑K₀) U K₁ ≤ MeasureTheory.Measure.haar.addPrehaar (↑K₀) U K₂

theorem MeasureTheory.Measure.haar.prehaar_mono {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] {K₀ : TopologicalSpace.PositiveCompacts G} {U : Set G} (hU : Set.Nonempty (interior U)) {K₁ : TopologicalSpace.Compacts G} {K₂ : TopologicalSpace.Compacts G} (h : ↑K₁ ⊆ K₂.carrier) : MeasureTheory.Measure.haar.prehaar (↑K₀) U K₁ ≤ MeasureTheory.Measure.haar.prehaar (↑K₀) U K₂

theorem MeasureTheory.Measure.haar.addPrehaar_self {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] {K₀ : TopologicalSpace.PositiveCompacts G} {U : Set G} (hU : Set.Nonempty (interior U)) : MeasureTheory.Measure.haar.addPrehaar (↑K₀) U K₀.toCompacts = 1

theorem MeasureTheory.Measure.haar.prehaar_self {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] {K₀ : TopologicalSpace.PositiveCompacts G} {U : Set G} (hU : Set.Nonempty (interior U)) : MeasureTheory.Measure.haar.prehaar (↑K₀) U K₀.toCompacts = 1

theorem MeasureTheory.Measure.haar.addPrehaar_sup_le {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] {K₀ : TopologicalSpace.PositiveCompacts G} {U : Set G} (K₁ : TopologicalSpace.Compacts G) (K₂ : TopologicalSpace.Compacts G) (hU : Set.Nonempty (interior U)) : MeasureTheory.Measure.haar.addPrehaar (↑K₀) U (K₁ ⊔ K₂) ≤ MeasureTheory.Measure.haar.addPrehaar (↑K₀) U K₁ + MeasureTheory.Measure.haar.addPrehaar (↑K₀) U K₂

theorem MeasureTheory.Measure.haar.prehaar_sup_le {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] {K₀ : TopologicalSpace.PositiveCompacts G} {U : Set G} (K₁ : TopologicalSpace.Compacts G) (K₂ : TopologicalSpace.Compacts G) (hU : Set.Nonempty (interior U)) : MeasureTheory.Measure.haar.prehaar (↑K₀) U (K₁ ⊔ K₂) ≤ MeasureTheory.Measure.haar.prehaar (↑K₀) U K₁ + MeasureTheory.Measure.haar.prehaar (↑K₀) U K₂

theorem MeasureTheory.Measure.haar.addPrehaar_sup_eq {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] {K₀ : TopologicalSpace.PositiveCompacts G} {U : Set G} {K₁ : TopologicalSpace.Compacts G} {K₂ : TopologicalSpace.Compacts G} (hU : Set.Nonempty (interior U)) (h : Disjoint (K₁.carrier + -U) (K₂.carrier + -U)) : MeasureTheory.Measure.haar.addPrehaar (↑K₀) U (K₁ ⊔ K₂) = MeasureTheory.Measure.haar.addPrehaar (↑K₀) U K₁ + MeasureTheory.Measure.haar.addPrehaar (↑K₀) U K₂

theorem MeasureTheory.Measure.haar.prehaar_sup_eq {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] {K₀ : TopologicalSpace.PositiveCompacts G} {U : Set G} {K₁ : TopologicalSpace.Compacts G} {K₂ : TopologicalSpace.Compacts G} (hU : Set.Nonempty (interior U)) (h : Disjoint (K₁.carrier * U⁻¹) (K₂.carrier * U⁻¹)) : MeasureTheory.Measure.haar.prehaar (↑K₀) U (K₁ ⊔ K₂) = MeasureTheory.Measure.haar.prehaar (↑K₀) U K₁ + MeasureTheory.Measure.haar.prehaar (↑K₀) U K₂

theorem MeasureTheory.Measure.haar.is_left_invariant_addPrehaar {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] {K₀ : TopologicalSpace.PositiveCompacts G} {U : Set G} (hU : Set.Nonempty (interior U)) (g : G) (K : TopologicalSpace.Compacts G) : MeasureTheory.Measure.haar.addPrehaar (↑K₀) U (TopologicalSpace.Compacts.map (fun b => g + b) (_ : Continuous fun b => g + b) K) = MeasureTheory.Measure.haar.addPrehaar (↑K₀) U K

theorem MeasureTheory.Measure.haar.is_left_invariant_prehaar {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] {K₀ : TopologicalSpace.PositiveCompacts G} {U : Set G} (hU : Set.Nonempty (interior U)) (g : G) (K : TopologicalSpace.Compacts G) : MeasureTheory.Measure.haar.prehaar (↑K₀) U (TopologicalSpace.Compacts.map (fun b => g * b) (_ : Continuous fun b => g * b) K) = MeasureTheory.Measure.haar.prehaar (↑K₀) U K

Lemmas about haarProduct

theorem MeasureTheory.Measure.haar.addPrehaar_mem_addHaarProduct {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) {U : Set G} (hU : Set.Nonempty (interior U)) : MeasureTheory.Measure.haar.addPrehaar (↑K₀) U ∈ MeasureTheory.Measure.haar.addHaarProduct ↑K₀

theorem MeasureTheory.Measure.haar.prehaar_mem_haarProduct {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) {U : Set G} (hU : Set.Nonempty (interior U)) : MeasureTheory.Measure.haar.prehaar (↑K₀) U ∈ MeasureTheory.Measure.haar.haarProduct ↑K₀

theorem MeasureTheory.Measure.haar.nonempty_iInter_clAddPrehaar {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) : Set.Nonempty (MeasureTheory.Measure.haar.addHaarProduct ↑K₀ ∩ ⋂ (V : TopologicalSpace.OpenNhdsOf 0), MeasureTheory.Measure.haar.clAddPrehaar (↑K₀) V)

theorem MeasureTheory.Measure.haar.nonempty_iInter_clPrehaar {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) : Set.Nonempty (MeasureTheory.Measure.haar.haarProduct ↑K₀ ∩ ⋂ (V : TopologicalSpace.OpenNhdsOf 1), MeasureTheory.Measure.haar.clPrehaar (↑K₀) V)

Lemmas about chaar

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

additive version of MeasureTheory.Measure.haar.chaar

noncomputable def MeasureTheory.Measure.haar.chaar {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup 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.

theorem MeasureTheory.Measure.haar.addCHaar_mem_addHaarProduct {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) : MeasureTheory.Measure.haar.addCHaar K₀ ∈ MeasureTheory.Measure.haar.addHaarProduct ↑K₀

theorem MeasureTheory.Measure.haar.chaar_mem_haarProduct {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) : MeasureTheory.Measure.haar.chaar K₀ ∈ MeasureTheory.Measure.haar.haarProduct ↑K₀

theorem MeasureTheory.Measure.haar.addCHaar_mem_clAddPrehaar {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) (V : TopologicalSpace.OpenNhdsOf 0) : MeasureTheory.Measure.haar.addCHaar K₀ ∈ MeasureTheory.Measure.haar.clAddPrehaar (↑K₀) V

theorem MeasureTheory.Measure.haar.chaar_mem_clPrehaar {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) (V : TopologicalSpace.OpenNhdsOf 1) : MeasureTheory.Measure.haar.chaar K₀ ∈ MeasureTheory.Measure.haar.clPrehaar (↑K₀) V

theorem MeasureTheory.Measure.haar.addCHaar_nonneg {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) (K : TopologicalSpace.Compacts G) : 0 ≤ MeasureTheory.Measure.haar.addCHaar K₀ K

theorem MeasureTheory.Measure.haar.chaar_nonneg {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) (K : TopologicalSpace.Compacts G) : 0 ≤ MeasureTheory.Measure.haar.chaar K₀ K

theorem MeasureTheory.Measure.haar.addCHaar_empty {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) : MeasureTheory.Measure.haar.addCHaar K₀ ⊥ = 0

theorem MeasureTheory.Measure.haar.chaar_empty {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) : MeasureTheory.Measure.haar.chaar K₀ ⊥ = 0

theorem MeasureTheory.Measure.haar.addCHaar_self {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) : MeasureTheory.Measure.haar.addCHaar K₀ K₀.toCompacts = 1

theorem MeasureTheory.Measure.haar.chaar_self {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) : MeasureTheory.Measure.haar.chaar K₀ K₀.toCompacts = 1

theorem MeasureTheory.Measure.haar.addCHaar_mono {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] {K₀ : TopologicalSpace.PositiveCompacts G} {K₁ : TopologicalSpace.Compacts G} {K₂ : TopologicalSpace.Compacts G} (h : ↑K₁ ⊆ ↑K₂) : MeasureTheory.Measure.haar.addCHaar K₀ K₁ ≤ MeasureTheory.Measure.haar.addCHaar K₀ K₂

theorem MeasureTheory.Measure.haar.chaar_mono {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] {K₀ : TopologicalSpace.PositiveCompacts G} {K₁ : TopologicalSpace.Compacts G} {K₂ : TopologicalSpace.Compacts G} (h : ↑K₁ ⊆ ↑K₂) : MeasureTheory.Measure.haar.chaar K₀ K₁ ≤ MeasureTheory.Measure.haar.chaar K₀ K₂

theorem MeasureTheory.Measure.haar.addCHaar_sup_le {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] {K₀ : TopologicalSpace.PositiveCompacts G} (K₁ : TopologicalSpace.Compacts G) (K₂ : TopologicalSpace.Compacts G) : MeasureTheory.Measure.haar.addCHaar K₀ (K₁ ⊔ K₂) ≤ MeasureTheory.Measure.haar.addCHaar K₀ K₁ + MeasureTheory.Measure.haar.addCHaar K₀ K₂

theorem MeasureTheory.Measure.haar.chaar_sup_le {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] {K₀ : TopologicalSpace.PositiveCompacts G} (K₁ : TopologicalSpace.Compacts G) (K₂ : TopologicalSpace.Compacts G) : MeasureTheory.Measure.haar.chaar K₀ (K₁ ⊔ K₂) ≤ MeasureTheory.Measure.haar.chaar K₀ K₁ + MeasureTheory.Measure.haar.chaar K₀ K₂

theorem MeasureTheory.Measure.haar.addCHaar_sup_eq {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [T2Space G] {K₀ : TopologicalSpace.PositiveCompacts G} {K₁ : TopologicalSpace.Compacts G} {K₂ : TopologicalSpace.Compacts G} (h : Disjoint K₁.carrier K₂.carrier) : MeasureTheory.Measure.haar.addCHaar K₀ (K₁ ⊔ K₂) = MeasureTheory.Measure.haar.addCHaar K₀ K₁ + MeasureTheory.Measure.haar.addCHaar K₀ K₂

theorem MeasureTheory.Measure.haar.chaar_sup_eq {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] [T2Space G] {K₀ : TopologicalSpace.PositiveCompacts G} {K₁ : TopologicalSpace.Compacts G} {K₂ : TopologicalSpace.Compacts G} (h : Disjoint K₁.carrier K₂.carrier) : MeasureTheory.Measure.haar.chaar K₀ (K₁ ⊔ K₂) = MeasureTheory.Measure.haar.chaar K₀ K₁ + MeasureTheory.Measure.haar.chaar K₀ K₂

theorem MeasureTheory.Measure.haar.is_left_invariant_addCHaar {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] {K₀ : TopologicalSpace.PositiveCompacts G} (g : G) (K : TopologicalSpace.Compacts G) : MeasureTheory.Measure.haar.addCHaar K₀ (TopologicalSpace.Compacts.map (fun b => g + b) (_ : Continuous fun b => g + b) K) = MeasureTheory.Measure.haar.addCHaar K₀ K

theorem MeasureTheory.Measure.haar.is_left_invariant_chaar {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] {K₀ : TopologicalSpace.PositiveCompacts G} (g : G) (K : TopologicalSpace.Compacts G) : MeasureTheory.Measure.haar.chaar K₀ (TopologicalSpace.Compacts.map (fun b => g * b) (_ : Continuous fun b => g * b) K) = MeasureTheory.Measure.haar.chaar K₀ K

theorem MeasureTheory.Measure.haar.addHaarContent.proof_3 {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) (K₁ : TopologicalSpace.Compacts G) (K₂ : TopologicalSpace.Compacts G) : (fun K => { val := MeasureTheory.Measure.haar.addCHaar K₀ K, property := (_ : 0 ≤ MeasureTheory.Measure.haar.addCHaar K₀ K) }) (K₁ ⊔ K₂) ≤ (fun K => { val := MeasureTheory.Measure.haar.addCHaar K₀ K, property := (_ : 0 ≤ MeasureTheory.Measure.haar.addCHaar K₀ K) }) K₁ + (fun K => { val := MeasureTheory.Measure.haar.addCHaar K₀ K, property := (_ : 0 ≤ MeasureTheory.Measure.haar.addCHaar K₀ K) }) K₂

theorem MeasureTheory.Measure.haar.addHaarContent.proof_2 {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [T2Space G] (K₀ : TopologicalSpace.PositiveCompacts G) (K₁ : TopologicalSpace.Compacts G) (K₂ : TopologicalSpace.Compacts G) (h : Disjoint ↑K₁ ↑K₂) : (fun K => { val := MeasureTheory.Measure.haar.addCHaar K₀ K, property := (_ : 0 ≤ MeasureTheory.Measure.haar.addCHaar K₀ K) }) (K₁ ⊔ K₂) = (fun K => { val := MeasureTheory.Measure.haar.addCHaar K₀ K, property := (_ : 0 ≤ MeasureTheory.Measure.haar.addCHaar K₀ K) }) K₁ + (fun K => { val := MeasureTheory.Measure.haar.addCHaar K₀ K, property := (_ : 0 ≤ MeasureTheory.Measure.haar.addCHaar K₀ K) }) K₂

theorem MeasureTheory.Measure.haar.addHaarContent.proof_1 {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) (K₁ : TopologicalSpace.Compacts G) (K₂ : TopologicalSpace.Compacts G) (h : ↑K₁ ⊆ ↑K₂) : { val := MeasureTheory.Measure.haar.addCHaar K₀ K₁, property := (_ : 0 ≤ MeasureTheory.Measure.haar.addCHaar K₀ K₁) } ≤ { val := MeasureTheory.Measure.haar.addCHaar K₀ K₂, property := (_ : 0 ≤ MeasureTheory.Measure.haar.addCHaar K₀ K₂) }

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

additive version of MeasureTheory.Measure.haar.haarContent

noncomputable def MeasureTheory.Measure.haar.haarContent {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] [T2Space G] (K₀ : TopologicalSpace.PositiveCompacts G) : MeasureTheory.Content G

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

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

theorem MeasureTheory.Measure.haar.addHaarContent_apply {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [T2Space G] (K₀ : TopologicalSpace.PositiveCompacts G) (K : TopologicalSpace.Compacts G) : (fun s => ↑(MeasureTheory.Content.toFun (MeasureTheory.Measure.haar.addHaarContent K₀) s)) K = ↑(let_fun this := { val := MeasureTheory.Measure.haar.addCHaar K₀ K, property := (_ : 0 ≤ MeasureTheory.Measure.haar.addCHaar K₀ K) }; this)

theorem MeasureTheory.Measure.haar.haarContent_apply {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] [T2Space G] (K₀ : TopologicalSpace.PositiveCompacts G) (K : TopologicalSpace.Compacts G) : (fun s => ↑(MeasureTheory.Content.toFun (MeasureTheory.Measure.haar.haarContent K₀) s)) K = ↑(let_fun this := { val := MeasureTheory.Measure.haar.chaar K₀ K, property := (_ : 0 ≤ MeasureTheory.Measure.haar.chaar K₀ K) }; this)

theorem MeasureTheory.Measure.haar.addHaarContent_self {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [T2Space G] {K₀ : TopologicalSpace.PositiveCompacts G} : (fun s => ↑(MeasureTheory.Content.toFun (MeasureTheory.Measure.haar.addHaarContent K₀) s)) K₀.toCompacts = 1

The variant of addCHaar_self for addHaarContent.

theorem MeasureTheory.Measure.haar.haarContent_self {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] [T2Space G] {K₀ : TopologicalSpace.PositiveCompacts G} : (fun s => ↑(MeasureTheory.Content.toFun (MeasureTheory.Measure.haar.haarContent K₀) s)) K₀.toCompacts = 1

The variant of chaar_self for haarContent

theorem MeasureTheory.Measure.haar.is_left_invariant_addHaarContent {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [T2Space G] {K₀ : TopologicalSpace.PositiveCompacts G} (g : G) (K : TopologicalSpace.Compacts G) : (fun s => ↑(MeasureTheory.Content.toFun (MeasureTheory.Measure.haar.addHaarContent K₀) s)) (TopologicalSpace.Compacts.map (fun b => g + b) (_ : Continuous fun b => g + b) K) = (fun s => ↑(MeasureTheory.Content.toFun (MeasureTheory.Measure.haar.addHaarContent K₀) s)) K

The variant of is_left_invariant_addCHaar for addHaarContent

theorem MeasureTheory.Measure.haar.is_left_invariant_haarContent {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] [T2Space G] {K₀ : TopologicalSpace.PositiveCompacts G} (g : G) (K : TopologicalSpace.Compacts G) : (fun s => ↑(MeasureTheory.Content.toFun (MeasureTheory.Measure.haar.haarContent K₀) s)) (TopologicalSpace.Compacts.map (fun b => g * b) (_ : Continuous fun b => g * b) K) = (fun s => ↑(MeasureTheory.Content.toFun (MeasureTheory.Measure.haar.haarContent K₀) s)) K

The variant of is_left_invariant_chaar for haarContent

theorem MeasureTheory.Measure.haar.addHaarContent_outerMeasure_self_pos {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [T2Space G] {K₀ : TopologicalSpace.PositiveCompacts G} : 0 < ↑(MeasureTheory.Content.outerMeasure (MeasureTheory.Measure.haar.addHaarContent K₀)) ↑K₀

theorem MeasureTheory.Measure.haar.haarContent_outerMeasure_self_pos {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] [T2Space G] {K₀ : TopologicalSpace.PositiveCompacts G} : 0 < ↑(MeasureTheory.Content.outerMeasure (MeasureTheory.Measure.haar.haarContent K₀)) ↑K₀

The Haar measure

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

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

theorem MeasureTheory.Measure.addHaarMeasure.proof_1 : IsScalarTower ENNReal ENNReal ENNReal

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

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

theorem MeasureTheory.Measure.addHaarMeasure_apply {G : Type u_1} [AddGroup G] [TopologicalSpace G] [T2Space G] [TopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] {K₀ : TopologicalSpace.PositiveCompacts G} {s : Set G} (hs : MeasurableSet s) : ↑↑(MeasureTheory.Measure.addHaarMeasure K₀) s = ↑(MeasureTheory.Content.outerMeasure (MeasureTheory.Measure.haar.addHaarContent K₀)) s / ↑(MeasureTheory.Content.outerMeasure (MeasureTheory.Measure.haar.addHaarContent K₀)) ↑K₀

theorem MeasureTheory.Measure.haarMeasure_apply {G : Type u_1} [Group G] [TopologicalSpace G] [T2Space G] [TopologicalGroup G] [MeasurableSpace G] [BorelSpace G] {K₀ : TopologicalSpace.PositiveCompacts G} {s : Set G} (hs : MeasurableSet s) : ↑↑(MeasureTheory.Measure.haarMeasure K₀) s = ↑(MeasureTheory.Content.outerMeasure (MeasureTheory.Measure.haar.haarContent K₀)) s / ↑(MeasureTheory.Content.outerMeasure (MeasureTheory.Measure.haar.haarContent K₀)) ↑K₀

instance MeasureTheory.Measure.isAddLeftInvariant_addHaarMeasure {G : Type u_1} [AddGroup G] [TopologicalSpace G] [T2Space G] [TopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] (K₀ : TopologicalSpace.PositiveCompacts G) : MeasureTheory.Measure.IsAddLeftInvariant (MeasureTheory.Measure.addHaarMeasure K₀)

theorem MeasureTheory.Measure.isAddLeftInvariant_addHaarMeasure.proof_1 {G : Type u_1} [AddGroup G] [TopologicalSpace G] [T2Space G] [TopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] (K₀ : TopologicalSpace.PositiveCompacts G) : MeasureTheory.Measure.IsAddLeftInvariant (MeasureTheory.Measure.addHaarMeasure K₀)

instance MeasureTheory.Measure.isMulLeftInvariant_haarMeasure {G : Type u_1} [Group G] [TopologicalSpace G] [T2Space G] [TopologicalGroup G] [MeasurableSpace G] [BorelSpace G] (K₀ : TopologicalSpace.PositiveCompacts G) : MeasureTheory.Measure.IsMulLeftInvariant (MeasureTheory.Measure.haarMeasure K₀)

theorem MeasureTheory.Measure.addHaarMeasure_self {G : Type u_1} [AddGroup G] [TopologicalSpace G] [T2Space G] [TopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] {K₀ : TopologicalSpace.PositiveCompacts G} : ↑↑(MeasureTheory.Measure.addHaarMeasure K₀) ↑K₀ = 1

theorem MeasureTheory.Measure.haarMeasure_self {G : Type u_1} [Group G] [TopologicalSpace G] [T2Space G] [TopologicalGroup G] [MeasurableSpace G] [BorelSpace G] {K₀ : TopologicalSpace.PositiveCompacts G} : ↑↑(MeasureTheory.Measure.haarMeasure K₀) ↑K₀ = 1

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

The additive Haar measure is regular.

theorem MeasureTheory.Measure.regular_addHaarMeasure.proof_1 {G : Type u_1} [AddGroup G] [TopologicalSpace G] [T2Space G] [TopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] {K₀ : TopologicalSpace.PositiveCompacts G} : MeasureTheory.Measure.Regular ((↑(MeasureTheory.Content.outerMeasure (MeasureTheory.Measure.haar.addHaarContent K₀)) ↑K₀)⁻¹ • MeasureTheory.Content.measure (MeasureTheory.Measure.haar.addHaarContent K₀))

instance MeasureTheory.Measure.regular_haarMeasure {G : Type u_1} [Group G] [TopologicalSpace G] [T2Space G] [TopologicalGroup G] [MeasurableSpace G] [BorelSpace G] {K₀ : TopologicalSpace.PositiveCompacts G} : MeasureTheory.Measure.Regular (MeasureTheory.Measure.haarMeasure K₀)

The Haar measure is regular.

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

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

theorem MeasureTheory.Measure.sigmaFinite_addHaarMeasure.proof_1 {G : Type u_1} [AddGroup G] [TopologicalSpace G] [T2Space G] [TopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] [TopologicalSpace.SecondCountableTopology G] {K₀ : TopologicalSpace.PositiveCompacts G} : MeasureTheory.SigmaFinite (MeasureTheory.Measure.addHaarMeasure K₀)

instance MeasureTheory.Measure.sigmaFinite_haarMeasure {G : Type u_1} [Group G] [TopologicalSpace G] [T2Space G] [TopologicalGroup G] [MeasurableSpace G] [BorelSpace G] [TopologicalSpace.SecondCountableTopology G] {K₀ : TopologicalSpace.PositiveCompacts G} : MeasureTheory.SigmaFinite (MeasureTheory.Measure.haarMeasure K₀)

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

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

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.

theorem MeasureTheory.Measure.isAddHaarMeasure_addHaarMeasure.proof_1 {G : Type u_1} [AddGroup G] [TopologicalSpace G] [T2Space G] [TopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] (K₀ : TopologicalSpace.PositiveCompacts G) : MeasureTheory.Measure.IsAddHaarMeasure (MeasureTheory.Measure.addHaarMeasure K₀)

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

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.

theorem MeasureTheory.Measure.addHaar.proof_1 {G : Type u_1} [AddGroup G] [TopologicalSpace G] [LocallyCompactSpace G] : Nonempty (TopologicalSpace.PositiveCompacts G)

@[reducible]

noncomputable def MeasureTheory.Measure.addHaar {G : Type u_1} [AddGroup G] [TopologicalSpace G] [T2Space G] [TopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] [LocallyCompactSpace G] : MeasureTheory.Measure G

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

@[reducible]

noncomputable def MeasureTheory.Measure.haar {G : Type u_1} [Group G] [TopologicalSpace G] [T2Space G] [TopologicalGroup G] [MeasurableSpace G] [BorelSpace G] [LocallyCompactSpace G] : MeasureTheory.Measure G

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

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

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

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

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

theorem MeasureTheory.Measure.addHaarMeasure_eq_iff {G : Type u_1} [AddGroup G] [TopologicalSpace G] [T2Space G] [TopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] [TopologicalSpace.SecondCountableTopology G] (K₀ : TopologicalSpace.PositiveCompacts G) (μ : MeasureTheory.Measure G) [MeasureTheory.SigmaFinite μ] [MeasureTheory.Measure.IsAddLeftInvariant μ] : MeasureTheory.Measure.addHaarMeasure K₀ = μ ↔ ↑↑μ ↑K₀ = 1

theorem MeasureTheory.Measure.haarMeasure_eq_iff {G : Type u_1} [Group G] [TopologicalSpace G] [T2Space G] [TopologicalGroup G] [MeasurableSpace G] [BorelSpace G] [TopologicalSpace.SecondCountableTopology G] (K₀ : TopologicalSpace.PositiveCompacts G) (μ : MeasureTheory.Measure G) [MeasureTheory.SigmaFinite μ] [MeasureTheory.Measure.IsMulLeftInvariant μ] : MeasureTheory.Measure.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.

theorem MeasureTheory.Measure.regular_of_isAddLeftInvariant {G : Type u_1} [AddGroup G] [TopologicalSpace G] [T2Space G] [TopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] [TopologicalSpace.SecondCountableTopology G] {μ : MeasureTheory.Measure G} [MeasureTheory.SigmaFinite μ] [MeasureTheory.Measure.IsAddLeftInvariant μ] {K : Set G} (hK : IsCompact K) (h2K : Set.Nonempty (interior K)) (hμK : ↑↑μ K ≠ ⊤) : MeasureTheory.Measure.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.

theorem MeasureTheory.Measure.regular_of_isMulLeftInvariant {G : Type u_1} [Group G] [TopologicalSpace G] [T2Space G] [TopologicalGroup G] [MeasurableSpace G] [BorelSpace G] [TopologicalSpace.SecondCountableTopology G] {μ : MeasureTheory.Measure G} [MeasureTheory.SigmaFinite μ] [MeasureTheory.Measure.IsMulLeftInvariant μ] {K : Set G} (hK : IsCompact K) (h2K : Set.Nonempty (interior K)) (hμK : ↑↑μ K ≠ ⊤) : MeasureTheory.Measure.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.

theorem MeasureTheory.Measure.isAddHaarMeasure_eq_smul_isAddHaarMeasure {G : Type u_1} [AddGroup G] [TopologicalSpace G] [T2Space G] [TopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] [TopologicalSpace.SecondCountableTopology G] [LocallyCompactSpace G] (μ : MeasureTheory.Measure G) (ν : MeasureTheory.Measure G) [MeasureTheory.Measure.IsAddHaarMeasure μ] [MeasureTheory.Measure.IsAddHaarMeasure ν] : ∃ c, c ≠ 0 ∧ c ≠ ⊤ ∧ μ = c • ν

theorem MeasureTheory.Measure.isHaarMeasure_eq_smul_isHaarMeasure {G : Type u_1} [Group G] [TopologicalSpace G] [T2Space G] [TopologicalGroup G] [MeasurableSpace G] [BorelSpace G] [TopologicalSpace.SecondCountableTopology G] [LocallyCompactSpace G] (μ : MeasureTheory.Measure G) (ν : MeasureTheory.Measure G) [MeasureTheory.Measure.IsHaarMeasure μ] [MeasureTheory.Measure.IsHaarMeasure ν] : ∃ c, c ≠ 0 ∧ c ≠ ⊤ ∧ μ = c • ν

theorem MeasureTheory.Measure.absolutelyContinuous_isAddHaarMeasure {G : Type u_1} [AddGroup G] [TopologicalSpace G] [T2Space G] [TopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] [TopologicalSpace.SecondCountableTopology G] [LocallyCompactSpace G] (μ : MeasureTheory.Measure G) (ν : MeasureTheory.Measure G) [MeasureTheory.SigmaFinite μ] [MeasureTheory.Measure.IsAddLeftInvariant μ] [MeasureTheory.Measure.IsAddHaarMeasure ν] : MeasureTheory.Measure.AbsolutelyContinuous μ ν

An invariant measure is absolutely continuous with respect to an additive Haar measure.

theorem MeasureTheory.Measure.absolutelyContinuous_isHaarMeasure {G : Type u_1} [Group G] [TopologicalSpace G] [T2Space G] [TopologicalGroup G] [MeasurableSpace G] [BorelSpace G] [TopologicalSpace.SecondCountableTopology G] [LocallyCompactSpace G] (μ : MeasureTheory.Measure G) (ν : MeasureTheory.Measure G) [MeasureTheory.SigmaFinite μ] [MeasureTheory.Measure.IsMulLeftInvariant μ] [MeasureTheory.Measure.IsHaarMeasure ν] : MeasureTheory.Measure.AbsolutelyContinuous μ ν

An invariant measure is absolutely continuous with respect to a Haar measure.

theorem MeasureTheory.Measure.regular_of_isAddHaarMeasure.proof_1 {G : Type u_1} [AddGroup G] [TopologicalSpace G] [T2Space G] [TopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] [TopologicalSpace.SecondCountableTopology G] [LocallyCompactSpace G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsAddHaarMeasure μ] : MeasureTheory.Measure.Regular μ

instance MeasureTheory.Measure.regular_of_isAddHaarMeasure {G : Type u_1} [AddGroup G] [TopologicalSpace G] [T2Space G] [TopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] [TopologicalSpace.SecondCountableTopology G] [LocallyCompactSpace G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsAddHaarMeasure μ] : MeasureTheory.Measure.Regular μ

instance MeasureTheory.Measure.regular_of_isHaarMeasure {G : Type u_1} [Group G] [TopologicalSpace G] [T2Space G] [TopologicalGroup G] [MeasurableSpace G] [BorelSpace G] [TopologicalSpace.SecondCountableTopology G] [LocallyCompactSpace G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsHaarMeasure μ] : MeasureTheory.Measure.Regular μ

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

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.

theorem MeasureTheory.Measure.div_mem_nhds_one_of_haar_pos {G : Type u_1} [Group G] [TopologicalSpace G] [T2Space G] [TopologicalGroup G] [MeasurableSpace G] [BorelSpace G] [TopologicalSpace.SecondCountableTopology G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsHaarMeasure μ] [LocallyCompactSpace G] (E : Set G) (hE : MeasurableSet E) (hEpos : 0 < ↑↑μ E) : E / E ∈ nhds 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 1.

instance MeasureTheory.Measure.IsAddHaarMeasure.isNegInvariant {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [T2Space G] [MeasurableSpace G] [BorelSpace G] [TopologicalSpace.SecondCountableTopology G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsAddHaarMeasure μ] [LocallyCompactSpace G] : MeasureTheory.Measure.IsNegInvariant μ

Any additive Haar measure is invariant under negation in an abelian group.

theorem MeasureTheory.Measure.IsAddHaarMeasure.isNegInvariant.proof_1 {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [T2Space G] [MeasurableSpace G] [BorelSpace G] [TopologicalSpace.SecondCountableTopology G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsAddHaarMeasure μ] [LocallyCompactSpace G] : MeasureTheory.Measure.IsNegInvariant μ

instance MeasureTheory.Measure.IsHaarMeasure.isInvInvariant {G : Type u_1} [CommGroup G] [TopologicalSpace G] [TopologicalGroup G] [T2Space G] [MeasurableSpace G] [BorelSpace G] [TopologicalSpace.SecondCountableTopology G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsHaarMeasure μ] [LocallyCompactSpace G] : MeasureTheory.Measure.IsInvInvariant μ

Any Haar measure is invariant under inversion in an abelian group.

theorem MeasureTheory.Measure.measurePreserving_zsmul {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [T2Space G] [MeasurableSpace G] [BorelSpace G] [TopologicalSpace.SecondCountableTopology G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsAddHaarMeasure μ] [CompactSpace G] [DivisibleBy G ℤ] {n : ℤ} (hn : n ≠ 0) : MeasureTheory.MeasurePreserving fun g => n • g

theorem MeasureTheory.Measure.measurePreserving_zpow {G : Type u_1} [CommGroup G] [TopologicalSpace G] [TopologicalGroup G] [T2Space G] [MeasurableSpace G] [BorelSpace G] [TopologicalSpace.SecondCountableTopology G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsHaarMeasure μ] [CompactSpace G] [RootableBy G ℤ] {n : ℤ} (hn : n ≠ 0) : MeasureTheory.MeasurePreserving fun g => g ^ n

theorem MeasureTheory.Measure.MeasurePreserving.zsmul {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [T2Space G] [MeasurableSpace G] [BorelSpace G] [TopologicalSpace.SecondCountableTopology G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsAddHaarMeasure μ] [CompactSpace G] [DivisibleBy G ℤ] {n : ℤ} (hn : n ≠ 0) {X : Type u_2} [MeasurableSpace X] {μ' : MeasureTheory.Measure X} {f : X → G} (hf : MeasureTheory.MeasurePreserving f) : MeasureTheory.MeasurePreserving fun x => n • f x

theorem MeasureTheory.Measure.MeasurePreserving.zpow {G : Type u_1} [CommGroup G] [TopologicalSpace G] [TopologicalGroup G] [T2Space G] [MeasurableSpace G] [BorelSpace G] [TopologicalSpace.SecondCountableTopology G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsHaarMeasure μ] [CompactSpace G] [RootableBy G ℤ] {n : ℤ} (hn : n ≠ 0) {X : Type u_2} [MeasurableSpace X] {μ' : MeasureTheory.Measure X} {f : X → G} (hf : MeasureTheory.MeasurePreserving f) : MeasureTheory.MeasurePreserving fun x => f x ^ n