# mathlibdocumentation

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 #

• measure_theory.is_fundamental_domain.smul_invariant_measure_map: given a subgroup Γ of a topological group 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 ⧸ Γ.

• measure_theory.is_fundamental_domain.is_mul_left_invariant_map: given 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 ⧸ Γ.

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.

theorem subgroup.smul_invariant_measure {G : Type u_1} [group G] [borel_space G] {μ : measure_theory.measure G} {Γ : subgroup G}  :

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]
(G Γ)

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

@[protected, instance]
def quotient_group.has_measurable_smul {G : Type u_1} [group G] [borel_space G] {Γ : subgroup G} [measurable_space (G Γ)] [borel_space (G Γ)] :
(G Γ)

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 ⧸ Γ.

theorem measure_theory.is_fundamental_domain.smul_invariant_measure_map {G : Type u_1} [group G] [borel_space G] {μ : measure_theory.measure G} {Γ : subgroup G} {𝓕 : set G} (h𝓕 : μ) [encodable Γ] [measurable_space (G Γ)] [borel_space (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 ⧸ Γ.

theorem measure_theory.is_add_fundamental_domain.is_add_left_invariant_map {G : Type u_1} [add_group G] [borel_space G] {μ : measure_theory.measure G} {Γ : add_subgroup G} {𝓕 : set G} (h𝓕 : μ) [encodable Γ] [measurable_space (G Γ)] [borel_space (G Γ)] [Γ.normal]  :

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 ⧸ Γ.

theorem measure_theory.is_fundamental_domain.is_mul_left_invariant_map {G : Type u_1} [group G] [borel_space G] {μ : measure_theory.measure G} {Γ : subgroup G} {𝓕 : set G} (h𝓕 : μ) [encodable Γ] [measurable_space (G Γ)] [borel_space (G Γ)] [Γ.normal]  :

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 ⧸ Γ.

theorem measure_theory.is_add_fundamental_domain.map_restrict_quotient {G : Type u_1} [add_group G] [borel_space G] {μ : measure_theory.measure G} {Γ : add_subgroup G} {𝓕 : set G} (h𝓕 : μ) [encodable Γ] [measurable_space (G Γ)] [borel_space (G Γ)] [t2_space (G Γ)] (K : topological_space.positive_compacts (G Γ)) [Γ.normal] (h𝓕_finite : μ 𝓕 < ) :

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 ⧸ Γ.

theorem measure_theory.is_fundamental_domain.map_restrict_quotient {G : Type u_1} [group G] [borel_space G] {μ : measure_theory.measure G} {Γ : subgroup G} {𝓕 : set G} (h𝓕 : μ) [encodable Γ] [measurable_space (G Γ)] [borel_space (G Γ)] [t2_space (G Γ)] (K : topological_space.positive_compacts (G Γ)) [Γ.normal] [μ.is_haar_measure] (h𝓕_finite : μ 𝓕 < ) :
= μ (𝓕 ⁻¹' K)

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 ⧸ Γ.