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 #

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

Measurability of the action of the additive topological group G on the left-coset space 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 ⧸ Γ.

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

theorem MeasureTheory.IsFundamentalDomain.map_restrict_quotient {G : Type u_1} [Group G] [MeasurableSpace G] [TopologicalSpace G] [TopologicalGroup G] [BorelSpace G] {μ : MeasureTheory.Measure G} {Γ : Subgroup G} {𝓕 : Set G} (h𝓕 : MeasureTheory.IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕) [Countable { x // x ∈ Γ }] [MeasurableSpace (G ⧸ Γ)] [BorelSpace (G ⧸ Γ)] [T2Space (G ⧸ Γ)] [TopologicalSpace.SecondCountableTopology (G ⧸ Γ)] (K : TopologicalSpace.PositiveCompacts (G ⧸ Γ)) [Subgroup.Normal Γ] [MeasureTheory.Measure.IsHaarMeasure μ] [MeasureTheory.Measure.IsMulRightInvariant μ] (h𝓕_finite : ↑↑μ 𝓕 < ⊤) :

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} [AddGroup G] [MeasurableSpace G] [TopologicalSpace G] [TopologicalAddGroup G] [BorelSpace G] {μ : MeasureTheory.Measure G} {Γ : AddSubgroup G} {𝓕 : Set G} (h𝓕 : MeasureTheory.IsAddFundamentalDomain { x // x ∈ ↑AddSubgroup.opposite Γ } 𝓕) [Countable { x // x ∈ Γ }] [MeasurableSpace (G ⧸ Γ)] [BorelSpace (G ⧸ Γ)] [T2Space (G ⧸ Γ)] [TopologicalSpace.SecondCountableTopology (G ⧸ Γ)] (K : TopologicalSpace.PositiveCompacts (G ⧸ Γ)) [AddSubgroup.Normal Γ] [MeasureTheory.Measure.IsAddHaarMeasure μ] [MeasureTheory.Measure.IsAddRightInvariant μ] (h𝓕_finite : ↑↑μ 𝓕 < ⊤) (c : NNReal) (h : ↑↑μ (𝓕 ∩ ↑(QuotientAddGroup.mk' Γ) ⁻¹' ↑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} [Group G] [MeasurableSpace G] [TopologicalSpace G] [TopologicalGroup G] [BorelSpace G] {μ : MeasureTheory.Measure G} {Γ : Subgroup G} {𝓕 : Set G} (h𝓕 : MeasureTheory.IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕) [Countable { x // x ∈ Γ }] [MeasurableSpace (G ⧸ Γ)] [BorelSpace (G ⧸ Γ)] [T2Space (G ⧸ Γ)] [TopologicalSpace.SecondCountableTopology (G ⧸ Γ)] (K : TopologicalSpace.PositiveCompacts (G ⧸ Γ)) [Subgroup.Normal Γ] [MeasureTheory.Measure.IsHaarMeasure μ] [MeasureTheory.Measure.IsMulRightInvariant μ] (h𝓕_finite : ↑↑μ 𝓕 < ⊤) (c : NNReal) (h : ↑↑μ (𝓕 ∩ ↑(QuotientGroup.mk' Γ) ⁻¹' ↑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} [AddGroup G] {Γ : AddSubgroup G} (motive : { x // x ∈ ↑AddSubgroup.opposite Γ } → Prop) :
(h : { x // x ∈ ↑AddSubgroup.opposite Γ }) → ((γ : Gᵃᵒᵖ) → (hγ : γ ∈ ↑AddSubgroup.opposite Γ) → motive { val := γ, property := hγ }) → motive h
Instances For
    theorem essSup_comp_quotientAddGroup_mk {G : Type u_1} [AddGroup G] [MeasurableSpace G] [TopologicalSpace G] [TopologicalAddGroup G] [BorelSpace G] {μ : MeasureTheory.Measure G} {Γ : AddSubgroup G} {𝓕 : Set G} (h𝓕 : MeasureTheory.IsAddFundamentalDomain { x // x ∈ ↑AddSubgroup.opposite Γ } 𝓕) [Countable { x // x ∈ Γ }] [MeasurableSpace (G ⧸ Γ)] [BorelSpace (G ⧸ Γ)] [MeasureTheory.Measure.IsAddRightInvariant μ] {g : G ⧸ Γ → ENNReal} (g_ae_measurable : AEMeasurable g) :
    essSup g (MeasureTheory.Measure.map QuotientAddGroup.mk (MeasureTheory.Measure.restrict μ 𝓕)) = 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} [Group G] [MeasurableSpace G] [TopologicalSpace G] [TopologicalGroup G] [BorelSpace G] {μ : MeasureTheory.Measure G} {Γ : Subgroup G} {𝓕 : Set G} (h𝓕 : MeasureTheory.IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕) [Countable { x // x ∈ Γ }] [MeasurableSpace (G ⧸ Γ)] [BorelSpace (G ⧸ Γ)] [MeasureTheory.Measure.IsMulRightInvariant μ] {g : G ⧸ Γ → ENNReal} (g_ae_measurable : AEMeasurable g) :
    essSup g (MeasureTheory.Measure.map QuotientGroup.mk (MeasureTheory.Measure.restrict μ 𝓕)) = 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 μ.

    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!

    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} [AddGroup G] [MeasurableSpace G] [TopologicalSpace G] [TopologicalAddGroup G] [BorelSpace G] {μ : MeasureTheory.Measure G} {Γ : AddSubgroup G} {𝓕 : Set G} (h𝓕 : MeasureTheory.IsAddFundamentalDomain { x // x ∈ ↑AddSubgroup.opposite Γ } 𝓕) [Countable { x // x ∈ Γ }] [MeasurableSpace (G ⧸ Γ)] [BorelSpace (G ⧸ Γ)] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasureTheory.Measure.IsAddRightInvariant μ] {f : G → E} (hf₁ : MeasureTheory.Integrable f) (hf₂ : MeasureTheory.AEStronglyMeasurable (QuotientAddGroup.automorphize f) (MeasureTheory.Measure.map QuotientAddGroup.mk (MeasureTheory.Measure.restrict μ 𝓕))) :
    ∫ (x : G), f x ∂μ = ∫ (x : G ⧸ Γ), QuotientAddGroup.automorphize f x ∂MeasureTheory.Measure.map QuotientAddGroup.mk (MeasureTheory.Measure.restrict μ 𝓕)

    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} [Group G] [MeasurableSpace G] [TopologicalSpace G] [TopologicalGroup G] [BorelSpace G] {μ : MeasureTheory.Measure G} {Γ : Subgroup G} {𝓕 : Set G} (h𝓕 : MeasureTheory.IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕) [Countable { x // x ∈ Γ }] [MeasurableSpace (G ⧸ Γ)] [BorelSpace (G ⧸ Γ)] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasureTheory.Measure.IsMulRightInvariant μ] {f : G → E} (hf₁ : MeasureTheory.Integrable f) (hf₂ : MeasureTheory.AEStronglyMeasurable (QuotientGroup.automorphize f) (MeasureTheory.Measure.map QuotientGroup.mk (MeasureTheory.Measure.restrict μ 𝓕))) :
    ∫ (x : G), f x ∂μ = ∫ (x : G ⧸ Γ), QuotientGroup.automorphize f x ∂MeasureTheory.Measure.map QuotientGroup.mk (MeasureTheory.Measure.restrict μ 𝓕)

    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} [Group G] [MeasurableSpace G] [TopologicalSpace G] [TopologicalGroup G] [BorelSpace G] {μ : MeasureTheory.Measure G} {Γ : Subgroup G} {𝓕 : Set G} (h𝓕 : MeasureTheory.IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕) [Countable { x // x ∈ Γ }] [MeasurableSpace (G ⧸ Γ)] [BorelSpace (G ⧸ Γ)] {K : Type u_2} [NormedField K] [NormedSpace ℝ K] [MeasureTheory.Measure.IsMulRightInvariant μ] {f : G → K} (f_ℒ_1 : MeasureTheory.Integrable f) {g : G ⧸ Γ → K} (hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map QuotientGroup.mk (MeasureTheory.Measure.restrict μ 𝓕))) (g_ℒ_infinity : essSup (fun x => ↑‖g x‖₊) (MeasureTheory.Measure.map QuotientGroup.mk (MeasureTheory.Measure.restrict μ 𝓕)) ≠ ⊤) (F_ae_measurable : MeasureTheory.AEStronglyMeasurable (QuotientGroup.automorphize f) (MeasureTheory.Measure.map QuotientGroup.mk (MeasureTheory.Measure.restrict μ 𝓕))) :
    ∫ (x : G), g ↑x * f x ∂μ = ∫ (x : G ⧸ Γ), g x * QuotientGroup.automorphize f x ∂MeasureTheory.Measure.map QuotientGroup.mk (MeasureTheory.Measure.restrict μ 𝓕)

    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'] [MeasurableSpace G'] [TopologicalSpace G'] [TopologicalAddGroup G'] [BorelSpace G'] {μ' : MeasureTheory.Measure G'} {Γ' : AddSubgroup G'} [Countable { x // x ∈ Γ' }] [MeasurableSpace (G' ⧸ Γ')] [BorelSpace (G' ⧸ Γ')] {𝓕' : Set G'} {K : Type u_3} [NormedField K] [NormedSpace ℝ K] [MeasureTheory.Measure.IsAddRightInvariant μ'] {f : G' → K} (f_ℒ_1 : MeasureTheory.Integrable f) {g : G' ⧸ Γ' → K} (hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map QuotientAddGroup.mk (MeasureTheory.Measure.restrict μ' 𝓕'))) (g_ℒ_infinity : essSup (fun x => ↑‖g x‖₊) (MeasureTheory.Measure.map QuotientAddGroup.mk (MeasureTheory.Measure.restrict μ' 𝓕')) ≠ ⊤) (F_ae_measurable : MeasureTheory.AEStronglyMeasurable (QuotientAddGroup.automorphize f) (MeasureTheory.Measure.map QuotientAddGroup.mk (MeasureTheory.Measure.restrict μ' 𝓕'))) (h𝓕 : MeasureTheory.IsAddFundamentalDomain { x // x ∈ ↑AddSubgroup.opposite Γ' } 𝓕') :
    ∫ (x : G'), g ↑x * f x ∂μ' = ∫ (x : G' ⧸ Γ'), g x * QuotientAddGroup.automorphize f x ∂MeasureTheory.Measure.map QuotientAddGroup.mk (MeasureTheory.Measure.restrict μ' 𝓕')

    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.