Documentation

Mathlib.MeasureTheory.Measure.Haar.Basic

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 MeasureTheory.Measure.Haar.Unique.

Main Declarations #

References #

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

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

additive version of MeasureTheory.Measure.haar.index

Equations
Instances For
    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.

    Equations
    Instances For
      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).

      Equations
      Instances For

        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
        Instances For

          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
          Instances For

            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 : (interior V).Nonempty) :
            ∃ (n : ), n Finset.card '' {t : Finset G | K gt, (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.

            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 : (interior V).Nonempty) :
            ∃ (n : ), n Finset.card '' {t : Finset G | K gt, (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.

            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 : (interior V).Nonempty) :
            ∃ (t : Finset G), K gt, (fun (h : G) => g + h) ⁻¹' V t.card = 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 : (interior V).Nonempty) :
            ∃ (t : Finset G), K gt, (fun (h : G) => g * h) ⁻¹' V t.card = MeasureTheory.Measure.haar.index 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 : (interior V).Nonempty) :
            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 : (interior V).Nonempty) (h : Disjoint (K₁.carrier + -V) (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 : (interior V).Nonempty) (h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * 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 : (interior V).Nonempty) (g : G) :
            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 : (interior V).Nonempty) :

            Lemmas about prehaar #

            theorem MeasureTheory.Measure.haar.addPrehaar_pos {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) {U : Set G} (hU : (interior U).Nonempty) {K : Set G} (h1K : IsCompact K) (h2K : (interior K).Nonempty) :
            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 : (interior U).Nonempty) {K : Set G} (h1K : IsCompact K) (h2K : (interior K).Nonempty) :
            0 < MeasureTheory.Measure.haar.prehaar (K₀) U { carrier := K, isCompact' := h1K }
            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 : (interior U).Nonempty) (h : Disjoint (K₁.carrier * U⁻¹) (K₂.carrier * U⁻¹)) :

            Lemmas about haarProduct #

            Lemmas about chaar #

            This is the "limit" of prehaar K₀ U K as U becomes a smaller and smaller open neighborhood of (1 : G). More precisely, it is defined to be an arbitrary element in the intersection of all the sets 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
            Instances For
              theorem MeasureTheory.Measure.haar.addHaarContent.proof_2 {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (K₀ : TopologicalSpace.PositiveCompacts G) (K₁ : TopologicalSpace.Compacts G) (K₂ : TopologicalSpace.Compacts G) (h : Disjoint K₁ K₂) (_h₁ : IsClosed K₁) (h₂ : IsClosed K₂) :
              (fun (K : TopologicalSpace.Compacts G) => MeasureTheory.Measure.haar.addCHaar K₀ K, ) (K₁ K₂) = (fun (K : TopologicalSpace.Compacts G) => MeasureTheory.Measure.haar.addCHaar K₀ K, ) K₁ + (fun (K : TopologicalSpace.Compacts G) => MeasureTheory.Measure.haar.addCHaar K₀ K, ) K₂

              additive version of MeasureTheory.Measure.haar.haarContent

              Equations
              Instances For

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

                Equations
                Instances For

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

                  The Haar measure #

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

                  Equations
                  Instances For

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

                    Equations
                    Instances For

                      The additive Haar measure is regular.

                      Equations
                      • =

                      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.

                      Equations
                      • =

                      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.

                      Equations
                      • =
                      @[reducible]

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

                      Equations
                      Instances For
                        @[reducible]

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

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

                          theorem MeasureTheory.Measure.sub_mem_nhds_zero_of_addHaar_pos {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] (μ : MeasureTheory.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.

                          theorem MeasureTheory.Measure.div_mem_nhds_one_of_haar_pos {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] [MeasurableSpace G] [BorelSpace G] (μ : MeasureTheory.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.

                          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 MeasureTheory.Measure.Haar.Unique.

                          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.

                          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.

                          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] [TopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] [SecondCountableTopology G] {μ : MeasureTheory.Measure G} [MeasureTheory.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.

                          theorem MeasureTheory.Measure.regular_of_isMulLeftInvariant {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] [MeasurableSpace G] [BorelSpace G] [SecondCountableTopology G] {μ : MeasureTheory.Measure G} [MeasureTheory.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.