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

## Main results #

• MeasureTheory.IsFundamentalDomain.smulInvariantMeasure_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 ⧸ Γ.

• MeasureTheory.IsFundamentalDomain.isMulLeftInvariant_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.

instance QuotientAddGroup.measurableVAdd {G : Type u_1} [] [] [] [] {Γ : } [MeasurableSpace (G Γ)] [BorelSpace (G Γ)] :

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

theorem QuotientAddGroup.measurableVAdd.proof_1 {G : Type u_1} [] [] [] [] {Γ : } [MeasurableSpace (G Γ)] [BorelSpace (G Γ)] :
instance QuotientGroup.measurableSMul {G : Type u_1} [] [] [] [] [] {Γ : } [MeasurableSpace (G Γ)] [BorelSpace (G Γ)] :

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

theorem MeasureTheory.IsAddFundamentalDomain.vaddInvariantMeasure_map {G : Type u_1} [] [] [] [] {μ : } {Γ : } {𝓕 : Set G} (h𝓕 : MeasureTheory.IsAddFundamentalDomain { x // x AddSubgroup.opposite Γ } 𝓕) [Countable { x // x Γ }] [MeasurableSpace (G Γ)] [BorelSpace (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 MeasureTheory.IsFundamentalDomain.smulInvariantMeasure_map {G : Type u_1} [] [] [] [] [] {μ : } {Γ : } {𝓕 : Set G} (h𝓕 : MeasureTheory.IsFundamentalDomain { x // x Subgroup.opposite Γ } 𝓕) [Countable { x // x Γ }] [MeasurableSpace (G Γ)] [BorelSpace (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 MeasureTheory.IsAddFundamentalDomain.isAddLeftInvariant_map {G : Type u_1} [] [] [] [] {μ : } {Γ : } {𝓕 : Set G} (h𝓕 : MeasureTheory.IsAddFundamentalDomain { x // x AddSubgroup.opposite Γ } 𝓕) [Countable { x // x Γ }] [MeasurableSpace (G Γ)] [BorelSpace (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 ⧸ Γ.

theorem MeasureTheory.IsFundamentalDomain.isMulLeftInvariant_map {G : Type u_1} [] [] [] [] [] {μ : } {Γ : } {𝓕 : Set G} (h𝓕 : MeasureTheory.IsFundamentalDomain { x // x Subgroup.opposite Γ } 𝓕) [Countable { x // x Γ }] [MeasurableSpace (G Γ)] [BorelSpace (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 ⧸ Γ.

theorem MeasureTheory.IsAddFundamentalDomain.map_restrict_quotient {G : Type u_1} [] [] [] [] {μ : } {Γ : } {𝓕 : Set G} (h𝓕 : MeasureTheory.IsAddFundamentalDomain { x // x AddSubgroup.opposite Γ } 𝓕) [Countable { x // x Γ }] [MeasurableSpace (G Γ)] [BorelSpace (G Γ)] [T2Space (G Γ)] (K : ) (h𝓕_finite : μ 𝓕 < ) :
= μ (𝓕 ↑() ⁻¹' 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 ⧸ Γ.

theorem MeasureTheory.IsFundamentalDomain.map_restrict_quotient {G : Type u_1} [] [] [] [] [] {μ : } {Γ : } {𝓕 : Set G} (h𝓕 : MeasureTheory.IsFundamentalDomain { x // x Subgroup.opposite Γ } 𝓕) [Countable { x // x Γ }] [MeasurableSpace (G Γ)] [BorelSpace (G Γ)] [T2Space (G Γ)] (K : ) [] (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 ⧸ Γ.

theorem MeasurePreservingQuotientAddGroup.mk' {G : Type u_1} [] [] [] [] {μ : } {Γ : } {𝓕 : Set G} (h𝓕 : MeasureTheory.IsAddFundamentalDomain { x // x AddSubgroup.opposite Γ } 𝓕) [Countable { x // x Γ }] [MeasurableSpace (G Γ)] [BorelSpace (G Γ)] [T2Space (G Γ)] (K : ) (h𝓕_finite : μ 𝓕 < ) (c : NNReal) (h : μ (𝓕 ↑() ⁻¹' K) = c) :

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 ⧸ Γ is measure-preserving between appropriate multiples of Haar measure on G and G ⧸ Γ.

theorem MeasurePreservingQuotientGroup.mk' {G : Type u_1} [] [] [] [] [] {μ : } {Γ : } {𝓕 : Set G} (h𝓕 : MeasureTheory.IsFundamentalDomain { x // x Subgroup.opposite Γ } 𝓕) [Countable { x // x Γ }] [MeasurableSpace (G Γ)] [BorelSpace (G Γ)] [T2Space (G Γ)] (K : ) [] (h𝓕_finite : μ 𝓕 < ) (c : NNReal) (h : μ (𝓕 ↑() ⁻¹' K) = c) :

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 ⧸ Γ is measure-preserving between appropriate multiples of Haar measure on G and G ⧸ Γ.

abbrev essSup_comp_quotientAddGroup_mk.match_1 {G : Type u_1} [] {Γ : } (motive : { x // x AddSubgroup.opposite Γ }Prop) :
(h : { x // x AddSubgroup.opposite Γ }) → ((γ : Gᵃᵒᵖ) → ( : γ AddSubgroup.opposite Γ) → motive { val := γ, property := }) → motive h
Instances For
theorem essSup_comp_quotientAddGroup_mk {G : Type u_1} [] [] [] [] {μ : } {Γ : } {𝓕 : Set G} (h𝓕 : MeasureTheory.IsAddFundamentalDomain { x // x AddSubgroup.opposite Γ } 𝓕) [Countable { x // x Γ }] [MeasurableSpace (G Γ)] [BorelSpace (G Γ)] {g : G ΓENNReal} (g_ae_measurable : ) :
essSup g (MeasureTheory.Measure.map QuotientAddGroup.mk ()) = essSup (fun x => g x) μ

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 μ.

theorem essSup_comp_quotientGroup_mk {G : Type u_1} [] [] [] [] [] {μ : } {Γ : } {𝓕 : Set G} (h𝓕 : MeasureTheory.IsFundamentalDomain { x // x Subgroup.opposite Γ } 𝓕) [Countable { x // x Γ }] [MeasurableSpace (G Γ)] [BorelSpace (G Γ)] {g : G ΓENNReal} (g_ae_measurable : ) :
essSup g (MeasureTheory.Measure.map QuotientGroup.mk ()) = essSup (fun x => g x) μ

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 μ.

theorem MeasureTheory.IsAddFundamentalDomain.absolutelyContinuous_map {G : Type u_1} [] [] [] [] {μ : } {Γ : } {𝓕 : Set G} (h𝓕 : MeasureTheory.IsAddFundamentalDomain { x // x AddSubgroup.opposite Γ } 𝓕) [Countable { x // x Γ }] [MeasurableSpace (G Γ)] [BorelSpace (G Γ)] :

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!

theorem MeasureTheory.IsFundamentalDomain.absolutelyContinuous_map {G : Type u_1} [] [] [] [] [] {μ : } {Γ : } {𝓕 : Set G} (h𝓕 : MeasureTheory.IsFundamentalDomain { x // x Subgroup.opposite Γ } 𝓕) [Countable { x // x Γ }] [MeasurableSpace (G Γ)] [BorelSpace (G Γ)] :

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!

theorem QuotientAddGroup.integral_eq_integral_automorphize {G : Type u_1} [] [] [] [] {μ : } {Γ : } {𝓕 : Set G} (h𝓕 : MeasureTheory.IsAddFundamentalDomain { x // x AddSubgroup.opposite Γ } 𝓕) [Countable { x // x Γ }] [MeasurableSpace (G Γ)] [BorelSpace (G Γ)] {E : Type u_2} [] {f : GE} (hf₁ : ) (hf₂ : MeasureTheory.AEStronglyMeasurable () (MeasureTheory.Measure.map QuotientAddGroup.mk ())) :
∫ (x : G), f xμ = ∫ (x : G Γ), MeasureTheory.Measure.map QuotientAddGroup.mk ()

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.

theorem QuotientGroup.integral_eq_integral_automorphize {G : Type u_1} [] [] [] [] [] {μ : } {Γ : } {𝓕 : Set G} (h𝓕 : MeasureTheory.IsFundamentalDomain { x // x Subgroup.opposite Γ } 𝓕) [Countable { x // x Γ }] [MeasurableSpace (G Γ)] [BorelSpace (G Γ)] {E : Type u_2} [] {f : GE} (hf₁ : ) (hf₂ : MeasureTheory.AEStronglyMeasurable () (MeasureTheory.Measure.map QuotientGroup.mk ())) :
∫ (x : G), f xμ = ∫ (x : G Γ), MeasureTheory.Measure.map QuotientGroup.mk ()

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.

theorem QuotientGroup.integral_mul_eq_integral_automorphize_mul {G : Type u_1} [] [] [] [] [] {μ : } {Γ : } {𝓕 : Set G} (h𝓕 : MeasureTheory.IsFundamentalDomain { x // x Subgroup.opposite Γ } 𝓕) [Countable { x // x Γ }] [MeasurableSpace (G Γ)] [BorelSpace (G Γ)] {K : Type u_2} [] [] {f : GK} (f_ℒ_1 : ) {g : G ΓK} (hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map QuotientGroup.mk ())) (g_ℒ_infinity : essSup (fun x => g x‖₊) (MeasureTheory.Measure.map QuotientGroup.mk ()) ) (F_ae_measurable : MeasureTheory.AEStronglyMeasurable () (MeasureTheory.Measure.map QuotientGroup.mk ())) :
∫ (x : G), g x * f xμ = ∫ (x : G Γ), g x * MeasureTheory.Measure.map QuotientGroup.mk ()

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.

theorem QuotientAddGroup.integral_mul_eq_integral_automorphize_mul {G' : Type u_2} [AddGroup G'] [] [] [] [] {μ' : } {Γ' : } [Countable { x // x Γ' }] [MeasurableSpace (G' Γ')] [BorelSpace (G' Γ')] {𝓕' : Set G'} {K : Type u_3} [] [] {f : G'K} (f_ℒ_1 : ) {g : G' Γ'K} (hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map QuotientAddGroup.mk ())) (g_ℒ_infinity : essSup (fun x => g x‖₊) (MeasureTheory.Measure.map QuotientAddGroup.mk ()) ) (F_ae_measurable : MeasureTheory.AEStronglyMeasurable () (MeasureTheory.Measure.map QuotientAddGroup.mk ())) (h𝓕 : MeasureTheory.IsAddFundamentalDomain { x // x AddSubgroup.opposite Γ' } 𝓕') :
∫ (x : G'), g x * f xμ' = ∫ (x : G' Γ'), g x * MeasureTheory.Measure.map QuotientAddGroup.mk ()

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.