Documentation

Mathlib.MeasureTheory.Measure.Haar.Unique

Uniqueness of Haar measure in locally compact groups #

Main results #

In a locally compact group, we prove that two left-invariant measures μ' and μ which are finite on compact sets coincide, up to a normalizing scalar that we denote with haarScalarFactor μ' μ, in the following sense:

To get genuine equality of measures, we typically need additional regularity assumptions:

In general, uniqueness statements for Haar measures in the literature make some assumption of regularity, either regularity or inner regularity. We have tried to minimize the assumptions in the theorems above, and cover the different results that exist in the literature.

Implementation #

The first result integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport is classical. To prove it, we use a change of variables to express integrals with respect to a left-invariant measure as integrals with respect to a given right-invariant measure (with a suitable density function). The uniqueness readily follows.

Uniqueness results for the measure of compact sets and open sets, without any regularity assumption, are significantly harder. They rely on the completion-regularity of the standard regular Haar measure. We follow McQuillan's answer at https://mathoverflow.net/questions/456670/.

On second-countable groups, one can arrive to slightly different uniqueness results by using that the operations are measurable. In particular, one can get uniqueness assuming σ-finiteness of the measures but discarding the assumption that they are finite on compact sets. See haarMeasure_unique in the file MeasureTheory.Measure.Haar.Basic.

References #

[Halmos, Measure Theory][halmos1950measure] [Fremlin, Measure Theory (volume 4)][fremlin_vol4]

theorem IsCompact.measure_eq_biInf_integral_hasCompactSupport {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] {k : Set X} (hk : IsCompact k) (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasureOnCompacts μ] [μ.InnerRegularCompactLTTop] [LocallyCompactSpace X] [RegularSpace X] :
μ k = ⨅ (f : X), ⨅ (_ : Continuous f), ⨅ (_ : HasCompactSupport f), ⨅ (_ : Set.EqOn f 1 k), ⨅ (_ : 0 f), ENNReal.ofReal (∫ (x : X), f xμ)

In a locally compact regular space with an inner regular measure, the measure of a compact set k is the infimum of the integrals of compactly supported functions equal to 1 on k.

The parameterized integral x ↦ ∫ y, g (y⁻¹ * x) ∂μ depends continuously on y when g is a compactly supported continuous function on a topological group G, and μ is finite on compact sets.

Uniqueness of integrals of compactly supported functions #

Two left invariant measures coincide when integrating continuous compactly supported functions, up to a scalar that we denote with haarScalarFactor μ' μ .

This is proved by relating the integral for arbitrary left invariant and right invariant measures, applying a version of Fubini. As one may use the same right invariant measure, this shows that two different left invariant measures will give the same integral, up to some fixed scalar.

theorem MeasureTheory.Measure.integral_isAddLeftInvariant_isAddRightInvariant_combo {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} {ν : MeasureTheory.Measure G} [MeasureTheory.IsFiniteMeasureOnCompacts μ] [MeasureTheory.IsFiniteMeasureOnCompacts ν] [μ.IsAddLeftInvariant] [ν.IsAddRightInvariant] [ν.IsOpenPosMeasure] {f : G} {g : G} (hf : Continuous f) (h'f : HasCompactSupport f) (hg : Continuous g) (h'g : HasCompactSupport g) (g_nonneg : 0 g) {x₀ : G} (g_pos : g x₀ 0) :
∫ (x : G), f xμ = (∫ (y : G), f y * (∫ (z : G), g (-z + y)ν)⁻¹ν) * ∫ (x : G), g xμ
theorem MeasureTheory.Measure.integral_isMulLeftInvariant_isMulRightInvariant_combo {G : Type u_1} [TopologicalSpace G] [Group G] [TopologicalGroup G] [MeasurableSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} {ν : MeasureTheory.Measure G} [MeasureTheory.IsFiniteMeasureOnCompacts μ] [MeasureTheory.IsFiniteMeasureOnCompacts ν] [μ.IsMulLeftInvariant] [ν.IsMulRightInvariant] [ν.IsOpenPosMeasure] {f : G} {g : G} (hf : Continuous f) (h'f : HasCompactSupport f) (hg : Continuous g) (h'g : HasCompactSupport g) (g_nonneg : 0 g) {x₀ : G} (g_pos : g x₀ 0) :
∫ (x : G), f xμ = (∫ (y : G), f y * (∫ (z : G), g (z⁻¹ * y)ν)⁻¹ν) * ∫ (x : G), g xμ

In a group with a left invariant measure μ and a right invariant measure ν, one can express integrals with respect to μ as integrals with respect to ν up to a constant scaling factor (given in the statement as ∫ x, g x ∂μ where g is a fixed reference function) and an explicit density y ↦ 1/∫ z, g (z⁻¹ * y) ∂ν.

theorem MeasureTheory.Measure.exists_integral_isAddLeftInvariant_eq_smul_of_hasCompactSupport {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] (μ' : MeasureTheory.Measure G) (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts μ'] [μ'.IsAddLeftInvariant] :
∃ (c : NNReal), ∀ (f : G), Continuous fHasCompactSupport f∫ (x : G), f xμ' = ∫ (x : G), f xc μ
theorem MeasureTheory.Measure.exists_integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport {G : Type u_1} [TopologicalSpace G] [Group G] [TopologicalGroup G] [MeasurableSpace G] [BorelSpace G] (μ' : MeasureTheory.Measure G) (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts μ'] [μ'.IsMulLeftInvariant] :
∃ (c : NNReal), ∀ (f : G), Continuous fHasCompactSupport f∫ (x : G), f xμ' = ∫ (x : G), f xc μ

Given two left-invariant measures which are finite on compacts, they coincide in the following sense: they give the same value to the integral of continuous compactly supported functions, up to a multiplicative constant.

Given two left-invariant measures which are finite on compacts, addHaarScalarFactor μ' μ is a scalar such that ∫ f dμ' = (addHaarScalarFactor μ' μ) ∫ f dμ for any compactly supported continuous function f.

Note that there is a dissymmetry in the assumptions between μ' and μ: the measure μ' needs only be finite on compact sets, while μ has to be finite on compact sets and positive on open sets, i.e., an additive Haar measure, to exclude for instance the case where μ = 0, where the definition doesn't make sense.

Equations
Instances For
    noncomputable def MeasureTheory.Measure.haarScalarFactor {G : Type u_1} [TopologicalSpace G] [Group G] [TopologicalGroup G] [MeasurableSpace G] [BorelSpace G] (μ' : MeasureTheory.Measure G) (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts μ'] [μ'.IsMulLeftInvariant] :

    Given two left-invariant measures which are finite on compacts, haarScalarFactor μ' μ is a scalar such that ∫ f dμ' = (haarScalarFactor μ' μ) ∫ f dμ for any compactly supported continuous function f.

    Note that there is a dissymmetry in the assumptions between μ' and μ: the measure μ' needs only be finite on compact sets, while μ has to be finite on compact sets and positive on open sets, i.e., a Haar measure, to exclude for instance the case where μ = 0, where the definition doesn't make sense.

    Equations
    Instances For
      theorem MeasureTheory.Measure.integral_isAddLeftInvariant_eq_smul_of_hasCompactSupport {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] (μ' : MeasureTheory.Measure G) (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts μ'] [μ'.IsAddLeftInvariant] {f : G} (hf : Continuous f) (h'f : HasCompactSupport f) :
      ∫ (x : G), f xμ' = ∫ (x : G), f xμ'.addHaarScalarFactor μ μ

      Two left invariant measures integrate in the same way continuous compactly supported functions, up to the scalar addHaarScalarFactor μ' μ. See also measure_isAddInvariant_eq_smul_of_isCompact_closure, which gives the same result for compact sets, and measure_isAddHaarMeasure_eq_smul_of_isOpen for open sets.

      theorem MeasureTheory.Measure.integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport {G : Type u_1} [TopologicalSpace G] [Group G] [TopologicalGroup G] [MeasurableSpace G] [BorelSpace G] (μ' : MeasureTheory.Measure G) (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts μ'] [μ'.IsMulLeftInvariant] {f : G} (hf : Continuous f) (h'f : HasCompactSupport f) :
      ∫ (x : G), f xμ' = ∫ (x : G), f xμ'.haarScalarFactor μ μ

      Two left invariant measures integrate in the same way continuous compactly supported functions, up to the scalar haarScalarFactor μ' μ. See also measure_isMulInvariant_eq_smul_of_isCompact_closure, which gives the same result for compact sets, and measure_isHaarMeasure_eq_smul_of_isOpen for open sets.

      theorem MeasureTheory.Measure.addHaarScalarFactor_eq_integral_div {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] (μ' : MeasureTheory.Measure G) (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts μ'] [μ'.IsAddLeftInvariant] {f : G} (hf : Continuous f) (h'f : HasCompactSupport f) (int_nonzero : ∫ (x : G), f xμ 0) :
      (μ'.addHaarScalarFactor μ) = (∫ (x : G), f xμ') / ∫ (x : G), f xμ
      theorem MeasureTheory.Measure.haarScalarFactor_eq_integral_div {G : Type u_1} [TopologicalSpace G] [Group G] [TopologicalGroup G] [MeasurableSpace G] [BorelSpace G] (μ' : MeasureTheory.Measure G) (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts μ'] [μ'.IsMulLeftInvariant] {f : G} (hf : Continuous f) (h'f : HasCompactSupport f) (int_nonzero : ∫ (x : G), f xμ 0) :
      (μ'.haarScalarFactor μ) = (∫ (x : G), f xμ') / ∫ (x : G), f xμ
      @[simp]
      theorem MeasureTheory.Measure.addHaarScalarFactor_smul {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] [LocallyCompactSpace G] (μ' : MeasureTheory.Measure G) (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts μ'] [μ'.IsAddLeftInvariant] {c : NNReal} :
      (c μ').addHaarScalarFactor μ = c μ'.addHaarScalarFactor μ
      @[simp]
      theorem MeasureTheory.Measure.haarScalarFactor_smul {G : Type u_1} [TopologicalSpace G] [Group G] [TopologicalGroup G] [MeasurableSpace G] [BorelSpace G] [LocallyCompactSpace G] (μ' : MeasureTheory.Measure G) (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts μ'] [μ'.IsMulLeftInvariant] {c : NNReal} :
      (c μ').haarScalarFactor μ = c μ'.haarScalarFactor μ
      @[simp]
      theorem MeasureTheory.Measure.addHaarScalarFactor_self {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] :
      μ.addHaarScalarFactor μ = 1
      @[simp]
      theorem MeasureTheory.Measure.haarScalarFactor_self {G : Type u_1} [TopologicalSpace G] [Group G] [TopologicalGroup G] [MeasurableSpace G] [BorelSpace G] (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] :
      μ.haarScalarFactor μ = 1
      theorem MeasureTheory.Measure.addHaarScalarFactor_eq_add {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] (μ' : MeasureTheory.Measure G) (μ : MeasureTheory.Measure G) (ν : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [ν.IsAddHaarMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts μ'] [μ'.IsAddLeftInvariant] :
      μ'.addHaarScalarFactor ν = μ'.addHaarScalarFactor μ * μ.addHaarScalarFactor ν
      theorem MeasureTheory.Measure.haarScalarFactor_eq_mul {G : Type u_1} [TopologicalSpace G] [Group G] [TopologicalGroup G] [MeasurableSpace G] [BorelSpace G] (μ' : MeasureTheory.Measure G) (μ : MeasureTheory.Measure G) (ν : MeasureTheory.Measure G) [μ.IsHaarMeasure] [ν.IsHaarMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts μ'] [μ'.IsMulLeftInvariant] :
      μ'.haarScalarFactor ν = μ'.haarScalarFactor μ * μ.haarScalarFactor ν
      theorem MeasureTheory.Measure.addHaarScalarFactor_pos_of_isAddHaarMeasure {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] (μ' : MeasureTheory.Measure G) (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [μ'.IsAddHaarMeasure] :
      0 < μ'.addHaarScalarFactor μ
      theorem MeasureTheory.Measure.haarScalarFactor_pos_of_isHaarMeasure {G : Type u_1} [TopologicalSpace G] [Group G] [TopologicalGroup G] [MeasurableSpace G] [BorelSpace G] (μ' : MeasureTheory.Measure G) (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [μ'.IsHaarMeasure] :
      0 < μ'.haarScalarFactor μ

      The scalar factor between two left-invariant measures is non-zero when both measures are positive on open sets.

      @[deprecated MeasureTheory.Measure.haarScalarFactor_pos_of_isHaarMeasure]
      theorem MeasureTheory.Measure.haarScalarFactor_pos_of_isOpenPosMeasure {G : Type u_1} [TopologicalSpace G] [Group G] [TopologicalGroup G] [MeasurableSpace G] [BorelSpace G] (μ' : MeasureTheory.Measure G) (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [μ'.IsHaarMeasure] :
      0 < μ'.haarScalarFactor μ

      Alias of MeasureTheory.Measure.haarScalarFactor_pos_of_isHaarMeasure.


      The scalar factor between two left-invariant measures is non-zero when both measures are positive on open sets.

      @[deprecated MeasureTheory.Measure.addHaarScalarFactor_pos_of_isAddHaarMeasure]
      theorem MeasureTheory.Measure.addHaarScalarFactor_pos_of_isOpenPosMeasure {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] (μ' : MeasureTheory.Measure G) (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [μ'.IsAddHaarMeasure] :
      0 < μ'.addHaarScalarFactor μ

      Alias of MeasureTheory.Measure.addHaarScalarFactor_pos_of_isAddHaarMeasure.

      Uniqueness of measure of sets with compact closure #

      Two left invariant measures give the same measure to sets with compact closure, up to the scalar haarScalarFactor μ' μ.

      This is a tricky argument, typically not done in textbooks (the textbooks version all require one version of regularity or another). Here is a sketch, based on McQuillan's answer at https://mathoverflow.net/questions/456670/.

      Assume for simplicity that all measures are normalized, so that the scalar factors are all 1. First, from the fact that μ and μ' integrate in the same way compactly supported functions, they give the same measure to compact "zero sets", i.e., sets of the form f⁻¹ {1} for f continuous and compactly supported. See measure_preimage_isMulLeftInvariant_eq_smul_of_hasCompactSupport.

      If μ is inner regular, a theorem of Halmos shows that any measurable set s of finite measure can be approximated from inside by a compact zero set k. Then μ s ≤ μ k + ε = μ' k + ε ≤ μ' s + ε. Letting ε tend to zero, one gets μ s ≤ μ' s. See smul_measure_isMulInvariant_le_of_isCompact_closure.

      Assume now that s is a measurable set of compact closure. It is contained in a compact zero set t. The same argument applied to t - s gives μ (t \ s) ≤ μ' (t \ s), i.e., μ t - μ s ≤ μ' t - μ' s. As μ t = μ' t (since these are zero sets), we get the inequality μ' s ≤ μ s. Together with the previous one, this gives μ' s = μ s. See measure_isMulInvariant_eq_smul_of_isCompact_closure_of_innerRegularCompactLTTop.

      If neither μ nor μ' is inner regular, we can use the existence of another inner regular left-invariant measure ν, so get μ s = ν s = μ' s, by applying twice the previous argument. Here, the uniqueness argument uses the existence of a Haar measure with a nice behavior! See measure_isMulInvariant_eq_smul_of_isCompact_closure_of_measurableSet.

      Finally, if s has compact closure but is not measurable, its measure is the infimum of the measures of its measurable supersets, and even of those contained in closure s. As μ and μ' coincide on these supersets, this yields μ s = μ' s. See measure_isMulInvariant_eq_smul_of_isCompact_closure.

      theorem MeasureTheory.Measure.measure_preimage_isAddLeftInvariant_eq_smul_of_hasCompactSupport {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] (μ' : MeasureTheory.Measure G) (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts μ'] [μ'.IsAddLeftInvariant] {f : G} (hf : Continuous f) (h'f : HasCompactSupport f) :
      μ' (f ⁻¹' {1}) = μ'.addHaarScalarFactor μ μ (f ⁻¹' {1})

      Two left invariant measures give the same mass to level sets of continuous compactly supported functions, up to the scalar addHaarScalarFactor μ' μ.

      Auxiliary lemma in the proof of the more general measure_isAddInvariant_eq_smul_of_isCompact_closure, which works for any set with compact closure.

      theorem MeasureTheory.Measure.measure_preimage_isMulLeftInvariant_eq_smul_of_hasCompactSupport {G : Type u_1} [TopologicalSpace G] [Group G] [TopologicalGroup G] [MeasurableSpace G] [BorelSpace G] (μ' : MeasureTheory.Measure G) (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts μ'] [μ'.IsMulLeftInvariant] {f : G} (hf : Continuous f) (h'f : HasCompactSupport f) :
      μ' (f ⁻¹' {1}) = μ'.haarScalarFactor μ μ (f ⁻¹' {1})

      Two left invariant measures give the same mass to level sets of continuous compactly supported functions, up to the scalar haarScalarFactor μ' μ.

      Auxiliary lemma in the proof of the more general measure_isMulInvariant_eq_smul_of_isCompact_closure, which works for any set with compact closure.

      theorem MeasureTheory.Measure.smul_measure_isAddInvariant_le_of_isCompact_closure {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] [LocallyCompactSpace G] (μ' : MeasureTheory.Measure G) (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts μ'] [μ'.IsAddLeftInvariant] [μ.InnerRegularCompactLTTop] {s : Set G} (hs : MeasurableSet s) (h's : IsCompact (closure s)) :
      μ'.addHaarScalarFactor μ μ s μ' s

      If an invariant measure is inner regular, then it gives less mass to sets with compact closure than any other invariant measure, up to the scalar addHaarScalarFactor μ' μ.

      Auxiliary lemma in the proof of the more general measure_isAddInvariant_eq_smul_of_isCompact_closure, which gives equality for any set with compact closure.

      theorem MeasureTheory.Measure.smul_measure_isMulInvariant_le_of_isCompact_closure {G : Type u_1} [TopologicalSpace G] [Group G] [TopologicalGroup G] [MeasurableSpace G] [BorelSpace G] [LocallyCompactSpace G] (μ' : MeasureTheory.Measure G) (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts μ'] [μ'.IsMulLeftInvariant] [μ.InnerRegularCompactLTTop] {s : Set G} (hs : MeasurableSet s) (h's : IsCompact (closure s)) :
      μ'.haarScalarFactor μ μ s μ' s

      If an invariant measure is inner regular, then it gives less mass to sets with compact closure than any other invariant measure, up to the scalar haarScalarFactor μ' μ.

      Auxiliary lemma in the proof of the more general measure_isMulInvariant_eq_smul_of_isCompact_closure, which gives equality for any set with compact closure.

      theorem MeasureTheory.Measure.measure_isAddInvariant_eq_smul_of_isCompact_closure_of_innerRegularCompactLTTop {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] [LocallyCompactSpace G] (μ' : MeasureTheory.Measure G) (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts μ'] [μ'.IsAddLeftInvariant] [μ.InnerRegularCompactLTTop] {s : Set G} (hs : MeasurableSet s) (h's : IsCompact (closure s)) :
      μ' s = μ'.addHaarScalarFactor μ μ s

      If an invariant measure is inner regular, then it gives the same mass to measurable sets with compact closure as any other invariant measure, up to the scalar addHaarScalarFactor μ' μ.

      Auxiliary lemma in the proof of the more general measure_isAddInvariant_eq_smul_of_isCompact_closure, which works for any set with compact closure, and removes the inner regularity assumption.

      theorem MeasureTheory.Measure.measure_isMulInvariant_eq_smul_of_isCompact_closure_of_innerRegularCompactLTTop {G : Type u_1} [TopologicalSpace G] [Group G] [TopologicalGroup G] [MeasurableSpace G] [BorelSpace G] [LocallyCompactSpace G] (μ' : MeasureTheory.Measure G) (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts μ'] [μ'.IsMulLeftInvariant] [μ.InnerRegularCompactLTTop] {s : Set G} (hs : MeasurableSet s) (h's : IsCompact (closure s)) :
      μ' s = μ'.haarScalarFactor μ μ s

      If an invariant measure is inner regular, then it gives the same mass to measurable sets with compact closure as any other invariant measure, up to the scalar haarScalarFactor μ' μ.

      Auxiliary lemma in the proof of the more general measure_isMulInvariant_eq_smul_of_isCompact_closure, which works for any set with compact closure, and removes the inner regularity assumption.

      Given an invariant measure then it gives the same mass to measurable sets with compact closure as any other invariant measure, up to the scalar addHaarScalarFactor μ' μ.

      Auxiliary lemma in the proof of the more general measure_isAddInvariant_eq_smul_of_isCompact_closure, which removes the measurability assumption.

      Given an invariant measure then it gives the same mass to measurable sets with compact closure as any other invariant measure, up to the scalar haarScalarFactor μ' μ.

      Auxiliary lemma in the proof of the more general measure_isMulInvariant_eq_smul_of_isCompact_closure, which removes the measurability assumption.

      theorem MeasureTheory.Measure.measure_isAddInvariant_eq_smul_of_isCompact_closure {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] [LocallyCompactSpace G] (μ' : MeasureTheory.Measure G) (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts μ'] [μ'.IsAddLeftInvariant] {s : Set G} (h's : IsCompact (closure s)) :
      μ' s = μ'.addHaarScalarFactor μ μ s

      Uniqueness of left-invariant measures: Given two left-invariant measures which are finite on compacts, they coincide in the following sense: they give the same value to sets with compact closure, up to the multiplicative constant addHaarScalarFactor μ' μ.

      theorem MeasureTheory.Measure.measure_isMulInvariant_eq_smul_of_isCompact_closure {G : Type u_1} [TopologicalSpace G] [Group G] [TopologicalGroup G] [MeasurableSpace G] [BorelSpace G] [LocallyCompactSpace G] (μ' : MeasureTheory.Measure G) (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts μ'] [μ'.IsMulLeftInvariant] {s : Set G} (h's : IsCompact (closure s)) :
      μ' s = μ'.haarScalarFactor μ μ s

      Uniqueness of left-invariant measures: Given two left-invariant measures which are finite on compacts, they coincide in the following sense: they give the same value to sets with compact closure, up to the multiplicative constant haarScalarFactor μ' μ.

      theorem MeasureTheory.Measure.isAddInvariant_eq_smul_of_compactSpace {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] [CompactSpace G] (μ' : MeasureTheory.Measure G) (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [μ'.IsAddLeftInvariant] [MeasureTheory.IsFiniteMeasureOnCompacts μ'] :
      μ' = μ'.addHaarScalarFactor μ μ
      theorem MeasureTheory.Measure.isMulInvariant_eq_smul_of_compactSpace {G : Type u_1} [TopologicalSpace G] [Group G] [TopologicalGroup G] [MeasurableSpace G] [BorelSpace G] [CompactSpace G] (μ' : MeasureTheory.Measure G) (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [μ'.IsMulLeftInvariant] [MeasureTheory.IsFiniteMeasureOnCompacts μ'] :
      μ' = μ'.haarScalarFactor μ μ

      Uniqueness of Haar measures: Two Haar measures on a compact group coincide up to a multiplicative factor.

      Uniqueness of Haar measures: Two Haar measures which are probability measures coincide.

      @[deprecated MeasureTheory.Measure.isHaarMeasure_eq_of_isProbabilityMeasure]

      Alias of MeasureTheory.Measure.isHaarMeasure_eq_of_isProbabilityMeasure.


      Uniqueness of Haar measures: Two Haar measures which are probability measures coincide.

      Uniqueness of measure of open sets #

      Two Haar measures give the same measure to open sets (or more generally to sets which are everywhere positive), up to the scalar haarScalarFactor μ' μ .

      theorem MeasureTheory.Measure.measure_isAddHaarMeasure_eq_smul_of_isEverywherePos {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] [LocallyCompactSpace G] (μ' : MeasureTheory.Measure G) (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [μ'.IsAddHaarMeasure] {s : Set G} (hs : MeasurableSet s) (h's : μ.IsEverywherePos s) :
      μ' s = μ'.addHaarScalarFactor μ μ s
      theorem MeasureTheory.Measure.measure_isHaarMeasure_eq_smul_of_isEverywherePos {G : Type u_1} [TopologicalSpace G] [Group G] [TopologicalGroup G] [MeasurableSpace G] [BorelSpace G] [LocallyCompactSpace G] (μ' : MeasureTheory.Measure G) (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [μ'.IsHaarMeasure] {s : Set G} (hs : MeasurableSet s) (h's : μ.IsEverywherePos s) :
      μ' s = μ'.haarScalarFactor μ μ s
      theorem MeasureTheory.Measure.measure_isAddHaarMeasure_eq_smul_of_isOpen {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] [LocallyCompactSpace G] (μ' : MeasureTheory.Measure G) (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [μ'.IsAddHaarMeasure] {s : Set G} (hs : IsOpen s) :
      μ' s = μ'.addHaarScalarFactor μ μ s

      Uniqueness of Haar measures: Given two additive Haar measures, they coincide in the following sense: they give the same value to open sets, up to the multiplicative constant addHaarScalarFactor μ' μ.

      theorem MeasureTheory.Measure.measure_isHaarMeasure_eq_smul_of_isOpen {G : Type u_1} [TopologicalSpace G] [Group G] [TopologicalGroup G] [MeasurableSpace G] [BorelSpace G] [LocallyCompactSpace G] (μ' : MeasureTheory.Measure G) (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [μ'.IsHaarMeasure] {s : Set G} (hs : IsOpen s) :
      μ' s = μ'.haarScalarFactor μ μ s

      Uniqueness of Haar measures: Given two Haar measures, they coincide in the following sense: they give the same value to open sets, up to the multiplicative constant haarScalarFactor μ' μ.

      Uniqueness of Haar measure under regularity assumptions. #

      theorem MeasureTheory.Measure.measure_isAddLeftInvariant_eq_vadd_of_ne_top {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] [LocallyCompactSpace G] (μ' : MeasureTheory.Measure G) (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts μ'] [μ'.IsAddLeftInvariant] [μ.InnerRegularCompactLTTop] [μ'.InnerRegularCompactLTTop] {s : Set G} (hs : μ s ) (h's : μ' s ) :
      μ' s = μ'.addHaarScalarFactor μ μ s
      theorem MeasureTheory.Measure.measure_isMulLeftInvariant_eq_smul_of_ne_top {G : Type u_1} [TopologicalSpace G] [Group G] [TopologicalGroup G] [MeasurableSpace G] [BorelSpace G] [LocallyCompactSpace G] (μ' : MeasureTheory.Measure G) (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts μ'] [μ'.IsMulLeftInvariant] [μ.InnerRegularCompactLTTop] [μ'.InnerRegularCompactLTTop] {s : Set G} (hs : μ s ) (h's : μ' s ) :
      μ' s = μ'.haarScalarFactor μ μ s

      Uniqueness of left-invariant measures: Given two left-invariant measures which are finite on compacts and inner regular for finite measure sets with respect to compact sets, they coincide in the following sense: they give the same value to finite measure sets, up to a multiplicative constant.

      theorem MeasureTheory.Measure.isAddLeftInvariant_eq_smul_of_innerRegular {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] [LocallyCompactSpace G] (μ' : MeasureTheory.Measure G) (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts μ'] [μ'.IsAddLeftInvariant] [μ.InnerRegular] [μ'.InnerRegular] :
      μ' = μ'.addHaarScalarFactor μ μ
      theorem MeasureTheory.Measure.isMulLeftInvariant_eq_smul_of_innerRegular {G : Type u_1} [TopologicalSpace G] [Group G] [TopologicalGroup G] [MeasurableSpace G] [BorelSpace G] [LocallyCompactSpace G] (μ' : MeasureTheory.Measure G) (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts μ'] [μ'.IsMulLeftInvariant] [μ.InnerRegular] [μ'.InnerRegular] :
      μ' = μ'.haarScalarFactor μ μ

      Uniqueness of left-invariant measures: Given two left-invariant measures which are finite on compacts and inner regular, they coincide up to a multiplicative constant.

      theorem MeasureTheory.Measure.isAddLeftInvariant_eq_smul_of_regular {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] [LocallyCompactSpace G] (μ' : MeasureTheory.Measure G) (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts μ'] [μ'.IsAddLeftInvariant] [μ.Regular] [μ'.Regular] :
      μ' = μ'.addHaarScalarFactor μ μ
      theorem MeasureTheory.Measure.isMulLeftInvariant_eq_smul_of_regular {G : Type u_1} [TopologicalSpace G] [Group G] [TopologicalGroup G] [MeasurableSpace G] [BorelSpace G] [LocallyCompactSpace G] (μ' : MeasureTheory.Measure G) (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts μ'] [μ'.IsMulLeftInvariant] [μ.Regular] [μ'.Regular] :
      μ' = μ'.haarScalarFactor μ μ

      Uniqueness of left-invariant measures: Given two left-invariant measures which are finite on compacts and regular, they coincide up to a multiplicative constant.

      Uniqueness of left-invariant measures: Two Haar measures coincide up to a multiplicative constant in a second countable group.

      @[deprecated MeasureTheory.Measure.isMulLeftInvariant_eq_smul]
      theorem MeasureTheory.Measure.isHaarMeasure_eq_smul {G : Type u_1} [TopologicalSpace G] [Group G] [TopologicalGroup G] [MeasurableSpace G] [BorelSpace G] [LocallyCompactSpace G] [SecondCountableTopology G] (μ' : MeasureTheory.Measure G) (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts μ'] [μ'.IsMulLeftInvariant] :
      μ' = μ'.haarScalarFactor μ μ

      Alias of MeasureTheory.Measure.isMulLeftInvariant_eq_smul.


      Uniqueness of left-invariant measures: Two Haar measures coincide up to a multiplicative constant in a second countable group.

      @[deprecated MeasureTheory.Measure.isAddLeftInvariant_eq_smul]
      theorem MeasureTheory.Measure.isAddHaarMeasure_eq_smul {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] [LocallyCompactSpace G] [SecondCountableTopology G] (μ' : MeasureTheory.Measure G) (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts μ'] [μ'.IsAddLeftInvariant] :
      μ' = μ'.addHaarScalarFactor μ μ

      Alias of MeasureTheory.Measure.isAddLeftInvariant_eq_smul.

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

      An invariant σ-finite measure is absolutely continuous with respect to a Haar measure in a second countable group.

      @[instance 100]

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

      Equations
      • =
      @[instance 100]

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

      Equations
      • =
      @[instance 100]

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

      Equations
      • =
      @[instance 100]

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

      Equations
      • =
      theorem MeasureTheory.Measure.MeasurePreserving.zsmul {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [CompactSpace G] [DivisibleBy G ] {n : } (hn : n 0) {X : Type u_2} [MeasurableSpace X] {μ' : MeasureTheory.Measure X} {f : XG} (hf : MeasureTheory.MeasurePreserving f μ' μ) :
      MeasureTheory.MeasurePreserving (fun (x : X) => n f x) μ' μ
      theorem MeasureTheory.Measure.MeasurePreserving.zpow {G : Type u_1} [CommGroup G] [TopologicalSpace G] [TopologicalGroup G] [MeasurableSpace G] [BorelSpace G] (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [CompactSpace G] [RootableBy G ] {n : } (hn : n 0) {X : Type u_2} [MeasurableSpace X] {μ' : MeasureTheory.Measure X} {f : XG} (hf : MeasureTheory.MeasurePreserving f μ' μ) :
      MeasureTheory.MeasurePreserving (fun (x : X) => f x ^ n) μ' μ