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:
integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport: they give the same value to the integral of continuous compactly supported functions, up to a scalar.measure_isMulInvariant_eq_smul_of_isCompact_closure: they give the same value to sets with compact closure, up to a scalar.measure_isHaarMeasure_eq_smul_of_isOpen: they give the same value to open sets, up to a scalar.
To get genuine equality of measures, we typically need additional regularity assumptions:
isMulLeftInvariant_eq_smul_of_innerRegular: two left invariant measures which are inner regular coincide up to a scalar.isMulLeftInvariant_eq_smul_of_regular: two left invariant measure which are regular coincide up to a scalar.isHaarMeasure_eq_smul: in a second countable space, two Haar measures coincide up to a scalar.isMulInvariant_eq_smul_of_compactSpace: two left-invariant measures on a compact group coincide up to a scalar.isHaarMeasure_eq_of_isProbabilityMeasure: two Haar measures which are probability measures coincide exactly.
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 Mathlib/MeasureTheory/Measure/Haar/Basic.lean.
References #
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.
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) ∂ν.
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, 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
- μ'.haarScalarFactor μ = if ¬LocallyCompactSpace G then 1 else ⋯.choose
Instances For
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
- μ'.addHaarScalarFactor μ = if ¬LocallyCompactSpace G then 1 else ⋯.choose
Instances For
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.
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.
The scalar factor between two left-invariant measures is non-zero when both measures are positive on open sets.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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 μ' μ.
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 μ' μ.
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.
Alias of MeasureTheory.Measure.isHaarMeasure_eq_of_isProbabilityMeasure.
Uniqueness of Haar measures: Two Haar measures which are probability measures coincide.
Alias of MeasureTheory.Measure.isAddHaarMeasure_eq_of_isProbabilityMeasure.
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 μ' μ .
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 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 μ' μ.
Uniqueness of Haar measure under regularity assumptions. #
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.
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.
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.
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.
An invariant σ-finite measure is absolutely continuous with respect to a Haar measure in a second countable group.
An invariant measure is absolutely continuous with respect to an additive Haar measure.
A continuous surjective monoid homomorphism of topological groups with compact codomain is measure preserving, provided that the Haar measures on the domain and on the codomain have the same total mass.
A continuous surjective additive monoid homomorphism of topological groups with compact codomain is measure preserving, provided that the Haar measures on the domain and on the codomain have the same total mass.
Any regular Haar measure is invariant under inversion in an abelian group.
Any regular additive Haar measure is invariant under negation in an abelian group.
Any inner regular Haar measure is invariant under inversion in an abelian group.
Any regular additive Haar measure is invariant under negation in an abelian group.