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.

source

theorem add_subgroup.vadd_invariant_measure {G : Type u_1} [add_group G] [measurable_space G] [topological_space G] [topological_add_group G] [borel_space G] {μ : measure_theory.measure G} {Γ : add_subgroup G} [μ.is_add_right_invariant] :

measure_theory.vadd_invariant_measure ↥(Γ.opposite) G μ

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.

source

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

measure_theory.smul_invariant_measure ↥(Γ.opposite) 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.

source

@[protected, instance]

def quotient_add_group.has_measurable_vadd {G : Type u_1} [add_group G] [measurable_space G] [topological_space G] [topological_add_group G] [borel_space G] {Γ : add_subgroup G} [measurable_space (G ⧸ Γ)] [borel_space (G ⧸ Γ)] :

has_measurable_vadd G (G ⧸ Γ)

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

source

@[protected, instance]

def quotient_group.has_measurable_smul {G : Type u_1} [group G] [measurable_space G] [topological_space G] [topological_group G] [borel_space G] {Γ : subgroup G} [measurable_space (G ⧸ Γ)] [borel_space (G ⧸ Γ)] :

has_measurable_smul G (G ⧸ Γ)

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

source

theorem measure_theory.is_fundamental_domain.smul {G : Type u_1} [group G] [measurable_space G] [topological_space G] [topological_group G] [borel_space G] {μ : measure_theory.measure G} {Γ : subgroup G} {𝓕 : set G} (h𝓕 : measure_theory.is_fundamental_domain ↥(Γ.opposite) 𝓕 μ) (g : G) [μ.is_mul_left_invariant] :

measure_theory.is_fundamental_domain ↥(Γ.opposite) (has_mul.mul g ⁻¹' 𝓕) μ

If 𝓕 is a fundamental domain for the action by right multiplication of a subgroup Γ of a topological group G, then its left-translate by an element of g is also a fundamental domain.

source

theorem measure_theory.is_add_fundamental_domain.vadd {G : Type u_1} [add_group G] [measurable_space G] [topological_space G] [topological_add_group G] [borel_space G] {μ : measure_theory.measure G} {Γ : add_subgroup G} {𝓕 : set G} (h𝓕 : measure_theory.is_add_fundamental_domain ↥(Γ.opposite) 𝓕 μ) (g : G) [μ.is_add_left_invariant] :

measure_theory.is_add_fundamental_domain ↥(Γ.opposite) (has_add.add g ⁻¹' 𝓕) μ

If 𝓕 is a fundamental domain for the action by right addition of a subgroup Γ of an additive topological group G, then its left-translate by an element of g is also a fundamental domain.

source

theorem measure_theory.is_add_fundamental_domain.vadd_invariant_measure_map {G : Type u_1} [add_group G] [measurable_space G] [topological_space G] [topological_add_group G] [borel_space G] {μ : measure_theory.measure G} {Γ : add_subgroup G} {𝓕 : set G} (h𝓕 : measure_theory.is_add_fundamental_domain ↥(Γ.opposite) 𝓕 μ) [encodable ↥Γ] [measurable_space (G ⧸ Γ)] [borel_space (G ⧸ Γ)] [μ.is_add_left_invariant] [μ.is_add_right_invariant] :

measure_theory.vadd_invariant_measure G (G ⧸ Γ) (⇑(measure_theory.measure.map quotient_add_group.mk) (μ.restrict 𝓕))

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

source

theorem measure_theory.is_fundamental_domain.smul_invariant_measure_map {G : Type u_1} [group G] [measurable_space G] [topological_space G] [topological_group G] [borel_space G] {μ : measure_theory.measure G} {Γ : subgroup G} {𝓕 : set G} (h𝓕 : measure_theory.is_fundamental_domain ↥(Γ.opposite) 𝓕 μ) [encodable ↥Γ] [measurable_space (G ⧸ Γ)] [borel_space (G ⧸ Γ)] [μ.is_mul_left_invariant] [μ.is_mul_right_invariant] :

measure_theory.smul_invariant_measure G (G ⧸ Γ) (⇑(measure_theory.measure.map quotient_group.mk) (μ.restrict 𝓕))

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

source

theorem measure_theory.is_add_fundamental_domain.is_add_left_invariant_map {G : Type u_1} [add_group G] [measurable_space G] [topological_space G] [topological_add_group G] [borel_space G] {μ : measure_theory.measure G} {Γ : add_subgroup G} {𝓕 : set G} (h𝓕 : measure_theory.is_add_fundamental_domain ↥(Γ.opposite) 𝓕 μ) [encodable ↥Γ] [measurable_space (G ⧸ Γ)] [borel_space (G ⧸ Γ)] [Γ.normal] [μ.is_add_left_invariant] [μ.is_add_right_invariant] :

(⇑(measure_theory.measure.map ⇑(quotient_add_group.mk' Γ)) (μ.restrict 𝓕)).is_add_left_invariant

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

source

theorem measure_theory.is_fundamental_domain.is_mul_left_invariant_map {G : Type u_1} [group G] [measurable_space G] [topological_space G] [topological_group G] [borel_space G] {μ : measure_theory.measure G} {Γ : subgroup G} {𝓕 : set G} (h𝓕 : measure_theory.is_fundamental_domain ↥(Γ.opposite) 𝓕 μ) [encodable ↥Γ] [measurable_space (G ⧸ Γ)] [borel_space (G ⧸ Γ)] [Γ.normal] [μ.is_mul_left_invariant] [μ.is_mul_right_invariant] :

(⇑(measure_theory.measure.map ⇑(quotient_group.mk' Γ)) (μ.restrict 𝓕)).is_mul_left_invariant

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

source

theorem measure_theory.is_add_fundamental_domain.map_restrict_quotient {G : Type u_1} [add_group G] [measurable_space G] [topological_space G] [topological_add_group G] [borel_space G] {μ : measure_theory.measure G} {Γ : add_subgroup G} {𝓕 : set G} (h𝓕 : measure_theory.is_add_fundamental_domain ↥(Γ.opposite) 𝓕 μ) [encodable ↥Γ] [measurable_space (G ⧸ Γ)] [borel_space (G ⧸ Γ)] [t2_space (G ⧸ Γ)] [topological_space.second_countable_topology (G ⧸ Γ)] (K : topological_space.positive_compacts (G ⧸ Γ)) [Γ.normal] [μ.is_add_haar_measure] [μ.is_add_right_invariant] (h𝓕_finite : ⇑μ 𝓕 < ⊤) :

⇑(measure_theory.measure.map ⇑(quotient_add_group.mk' Γ)) (μ.restrict 𝓕) = ⇑μ (𝓕 ∩ ⇑(quotient_add_group.mk' Γ) ⁻¹' K.val) • measure_theory.measure.add_haar_measure K

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

source

theorem measure_theory.is_fundamental_domain.map_restrict_quotient {G : Type u_1} [group G] [measurable_space G] [topological_space G] [topological_group G] [borel_space G] {μ : measure_theory.measure G} {Γ : subgroup G} {𝓕 : set G} (h𝓕 : measure_theory.is_fundamental_domain ↥(Γ.opposite) 𝓕 μ) [encodable ↥Γ] [measurable_space (G ⧸ Γ)] [borel_space (G ⧸ Γ)] [t2_space (G ⧸ Γ)] [topological_space.second_countable_topology (G ⧸ Γ)] (K : topological_space.positive_compacts (G ⧸ Γ)) [Γ.normal] [μ.is_haar_measure] [μ.is_mul_right_invariant] (h𝓕_finite : ⇑μ 𝓕 < ⊤) :

⇑(measure_theory.measure.map ⇑(quotient_group.mk' Γ)) (μ.restrict 𝓕) = ⇑μ (𝓕 ∩ ⇑(quotient_group.mk' Γ) ⁻¹' K.val) • measure_theory.measure.haar_measure 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 ⧸ Γ.