Haar quotient measure #
In this file, we consider properties of fundamental domains and measures for the action of a
subgroup Γ of a topological group G on G itself. Let μ be a measure on G ⧸ Γ.
Main results #
MeasureTheory.QuotientMeasureEqMeasurePreimage.smulInvariantMeasure_quotient: IfμsatisfiesQuotientMeasureEqMeasurePreimagerelative to a both left- and right-invariant measure onG, then it is aGinvariant measure onG ⧸ Γ.
The next two results assume that Γ is normal, and that G is equipped with a left- and
right-invariant measure.
MeasureTheory.QuotientMeasureEqMeasurePreimage.mulInvariantMeasure_quotient: IfμsatisfiesQuotientMeasureEqMeasurePreimage, thenμis a left-invariant measure.MeasureTheory.leftInvariantIsQuotientMeasureEqMeasurePreimage: Ifμis left-invariant, and the action ofΓonGhas finite covolume, andμsatisfies the right scaling condition, then it satisfiesQuotientMeasureEqMeasurePreimage. This is a converse toMeasureTheory.QuotientMeasureEqMeasurePreimage.mulInvariantMeasure_quotient.
The last result assumes that G is locally compact, that Γ is countable and normal, that its
action on G has a fundamental domain, and that μ is a finite measure. We also assume that G
is equipped with a sigma-finite Haar measure.
MeasureTheory.QuotientMeasureEqMeasurePreimage.haarMeasure_quotient: IfμsatisfiesQuotientMeasureEqMeasurePreimage, then it is itself Haar. This is a variant ofMeasureTheory.QuotientMeasureEqMeasurePreimage.mulInvariantMeasure_quotient.
Note that a group G with Haar measure that is both left and right invariant is called
unimodular.
Measurability of the action of the topological group G on the left-coset space G / Γ.
Measurability of the action of the additive topological group G on the left-coset
space G / Γ.
Given a subgroup Γ of a topological group G with measure ν, and a measure 'μ' on the
quotient G ⧸ Γ satisfying QuotientMeasureEqMeasurePreimage, the restriction
of ν to a fundamental domain is measure-preserving with respect to μ.
If μ satisfies QuotientMeasureEqMeasurePreimage relative to a both left- and right-
invariant measure ν on G, then it is a G invariant measure on G ⧸ Γ.
If μ on G ⧸ Γ satisfies QuotientMeasureEqMeasurePreimage relative to a both left- and
right-invariant measure on G and Γ is a normal subgroup, then μ is a left-invariant
measure.
If μ on G ⧸ Γ satisfies AddQuotientMeasureEqMeasurePreimage relative to a both
left- and right-invariant measure on G and Γ is a normal subgroup, then μ is a
left-invariant measure.
Assume that a measure μ is IsMulLeftInvariant, that the action of Γ on G has a
measurable fundamental domain s with positive finite volume, and that there is a single measurable
set V ⊆ G ⧸ Γ along which the pullback of μ and ν agree (so the scaling is right). Then
μ satisfies QuotientMeasureEqMeasurePreimage. The main tool of the proof is the uniqueness of
left invariant measures, if normalized by a single positive finite-measured set.
Assume that a measure μ is IsAddLeftInvariant, that the action of Γ on G has a
measurable fundamental domain s with positive finite volume, and that there is a single measurable
set V ⊆ G ⧸ Γ along which the pullback of μ and ν agree (so the scaling is right). Then
μ satisfies AddQuotientMeasureEqMeasurePreimage. The main tool of the proof is the uniqueness of
left invariant measures, if normalized by a single positive finite-measured set.
If a measure μ is left-invariant and satisfies the right scaling condition, then it
satisfies QuotientMeasureEqMeasurePreimage.
If a measure μ is
left-invariant and satisfies the right scaling condition, then it satisfies
AddQuotientMeasureEqMeasurePreimage.
If a measure μ on the quotient G ⧸ Γ of a group G by a discrete normal subgroup Γ having
fundamental domain, satisfies QuotientMeasureEqMeasurePreimage relative to a standardized choice
of Haar measure on G, and assuming μ is finite, then μ is itself Haar.
TODO: Is it possible to drop the assumption that μ is finite?
If a measure μ on the quotient G ⧸ Γ of an additive group G by a discrete
normal subgroup Γ having fundamental domain, satisfies AddQuotientMeasureEqMeasurePreimage
relative to a standardized choice of Haar measure on G, and assuming μ is finite, then μ is
itself Haar.
Given a normal subgroup Γ of a topological group G with Haar measure μ, which is also
right-invariant, and a finite volume fundamental domain 𝓕, the quotient map to G ⧸ Γ,
properly normalized, satisfies QuotientMeasureEqMeasurePreimage.
Given a normal
subgroup Γ of an additive topological group G with Haar measure μ, which is also
right-invariant, and a finite volume fundamental domain 𝓕, the quotient map to G ⧸ Γ,
properly normalized, satisfies AddQuotientMeasureEqMeasurePreimage.
Given a normal subgroup Γ of a topological group G with Haar measure μ, which is also
right-invariant, and a finite volume fundamental domain 𝓕, the quotient map to G ⧸ Γ,
properly normalized, satisfies QuotientMeasureEqMeasurePreimage.
Given a
normal subgroup Γ of an additive topological group G with Haar measure μ, which is also
right-invariant, and a finite volume fundamental domain 𝓕, the quotient map to G ⧸ Γ,
properly normalized, satisfies AddQuotientMeasureEqMeasurePreimage.
The essSup of a function g on the quotient space G ⧸ Γ with respect to the pushforward
of the restriction, μ_𝓕, of a right-invariant measure μ to a fundamental domain 𝓕, is the
same as the essSup of g's lift to the universal cover G with respect to μ.
The essSup of a function g on the additive quotient space G ⧸ Γ with respect
to the pushforward of the restriction, μ_𝓕, of a right-invariant measure μ to a fundamental
domain 𝓕, is the same as the essSup of g's lift to the universal cover G with respect
to μ.
Given a quotient space G ⧸ Γ where Γ is Countable, and the restriction,
μ_𝓕, of a right-invariant measure μ on G to a fundamental domain 𝓕, a set
in the quotient which has μ_𝓕-measure zero, also has measure zero under the
folding of μ under the quotient. Note that, if Γ is infinite, then the folded map
will take the value ∞ on any open set in the quotient!
Given an additive quotient space G ⧸ Γ where Γ is Countable, and the
restriction, μ_𝓕, of a right-invariant measure μ on G to a fundamental domain 𝓕, a set
in the quotient which has μ_𝓕-measure zero, also has measure zero under the
folding of μ under the quotient. Note that, if Γ is infinite, then the folded map
will take the value ∞ on any open set in the quotient!
This is a simple version of the Unfolding Trick: Given a subgroup Γ of a group G, the
integral of a function f on G with respect to a right-invariant measure μ is equal to the
integral over the quotient G ⧸ Γ of the automorphization of f.
This is a simple version of the Unfolding Trick: Given a subgroup Γ of an
additive group G, the integral of a function f on G with respect to a right-invariant
measure μ is equal to the integral over the quotient G ⧸ Γ of the automorphization of f.
This is the Unfolding Trick: Given a subgroup Γ of a group G, the integral of a
function f on G times the lift to G of a function g on the quotient G ⧸ Γ with respect
to a right-invariant measure μ on G, is equal to the integral over the quotient of the
automorphization of f times g.
This is the Unfolding Trick: Given an additive subgroup Γ' of an additive group G', the
integral of a function f on G' times the lift to G' of a function g on the quotient
G' ⧸ Γ' with respect to a right-invariant measure μ on G', is equal to the integral over
the quotient of the automorphization of f times g.