Documentation

Mathlib.MeasureTheory.Measure.Haar.Quotient

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 #

The next two results assume that Γ is normal, and that G is equipped with a left- and right-invariant measure.

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.

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.