Uniqueness of Haar measure in locally compact groups #
In a locally compact group, we prove that two left-invariant measures which are finite on compact
sets give the same value to the integral of continuous compactly supported functions, in
integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport. From this, we deduce various uniqueness
statements for left invariant measures (up to scalar multiplication):
measure_isMulLeftInvariant_eq_smul_of_ne_top: two left-invariant measures which are inner regular for finite measure sets with respect to compact sets give the same measure to compact sets.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.isMulLeftInvariant_eq_of_isProbabilityMeasure: two left-invariant probability measures which are inner regular for finite measure sets with respect to compact sets coincide.
The scalar factor that appears in these identities is defined as haarScalarFactor μ' μ.
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 (notably in integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport, which doesn't
make any regularity assumption), and cover the different results that exist in the literature.
The main result is integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport, and the other ones
follow readily from this one by using continuous compactly supported functions to approximate
characteristic functions of set.
To prove integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport, 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.
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.
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.
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) ∂ν.
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 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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The scalar factor between two left-invariant measures is non-zero when both measures are positive on open sets.
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.
Uniqueness of left-invariant measures: Given two left-invariant probability measures which are inner regular for finite measure sets with respect to compact sets, they coincide.
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.
Any regular additive Haar measure is invariant under negation in an abelian group.
Equations
Any regular Haar measure is invariant under inversion in an abelian group.
Equations
Any regular additive Haar measure is invariant under negation in an abelian group.
Equations
Any inner regular Haar measure is invariant under inversion in an abelian group.