mathlib documentation

measure_theory.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 group G on G itself.

Main results #

Note that a group G with Haar measure that is both left and right invariant is called unimodular.

Given a subgroup Γ of an additive group G and a right invariant measure μ on G, the measure is also invariant under the action of Γ on G by right addition.

Given a subgroup Γ of G and a right invariant measure μ on G, the measure is also invariant under the action of Γ on G by right multiplication.

@[protected, instance]

Measurability of the action of the additive topological group G on the left-coset space G/Γ.

@[protected, instance]

Measurability of the action of the topological group G on the left-coset space G/Γ.

The pushforward to the coset space G ⧸ Γ of the restriction of a both left- and right-invariant measure on an additive topological group G to a fundamental domain 𝓕 is a G-invariant measure on G ⧸ Γ.

The pushforward to the coset space G ⧸ Γ of the restriction of a both left- and right- invariant measure on G to a fundamental domain 𝓕 is a G-invariant measure on G ⧸ Γ.

Assuming Γ is a normal subgroup of an additive topological group G, the pushforward to the quotient group G ⧸ Γ of the restriction of a both left- and right-invariant measure on G to a fundamental domain 𝓕 is a left-invariant measure on G ⧸ Γ.

Assuming Γ is a normal subgroup of a topological group G, the pushforward to the quotient group G ⧸ Γ of the restriction of a both left- and right-invariant measure on G to a fundamental domain 𝓕 is a left-invariant measure on G ⧸ Γ.

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 pushforward to the quotient group G ⧸ Γ of the restriction of μ to 𝓕 is a multiple of Haar measure on G ⧸ Γ.

Given a normal subgroup Γ of a topological group G with Haar measure μ, which is also right-invariant, and a finite volume fundamental domain 𝓕, the pushforward to the quotient group G ⧸ Γ of the restriction of μ to 𝓕 is a multiple of Haar measure on G ⧸ Γ.