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

Equations
  • =

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

Equations
  • =

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

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

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 : (AddSubgroup.op Γ)Prop) :
∀ (h : (AddSubgroup.op Γ)), (∀ (γ : Gᵃᵒᵖ) ( : γ AddSubgroup.op Γ), motive { val := γ, property := })motive h
Equations
  • =
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 ((AddSubgroup.op Γ)) 𝓕 μ) [Countable Γ] [MeasurableSpace (G Γ)] [BorelSpace (G Γ)] [MeasureTheory.Measure.IsAddRightInvariant μ] {g : G ΓENNReal} (g_ae_measurable : AEMeasurable g (MeasureTheory.Measure.map QuotientAddGroup.mk (MeasureTheory.Measure.restrict μ 𝓕))) :
    essSup g (MeasureTheory.Measure.map QuotientAddGroup.mk (MeasureTheory.Measure.restrict μ 𝓕)) = essSup (fun (x : G) => 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 ((Subgroup.op Γ)) 𝓕 μ) [Countable Γ] [MeasurableSpace (G Γ)] [BorelSpace (G Γ)] [MeasureTheory.Measure.IsMulRightInvariant μ] {g : G ΓENNReal} (g_ae_measurable : AEMeasurable g (MeasureTheory.Measure.map QuotientGroup.mk (MeasureTheory.Measure.restrict μ 𝓕))) :
    essSup g (MeasureTheory.Measure.map QuotientGroup.mk (MeasureTheory.Measure.restrict μ 𝓕)) = essSup (fun (x : G) => 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!

    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.

    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 ((Subgroup.op Γ)) 𝓕 μ) [Countable Γ] [MeasurableSpace (G Γ)] [BorelSpace (G Γ)] {K : Type u_2} [NormedField K] [NormedSpace K] [MeasureTheory.Measure.IsMulRightInvariant μ] {f : GK} (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 Γ) => 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 xMeasureTheory.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 Γ'] [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' Γ') => 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 ((AddSubgroup.op Γ')) 𝓕' μ') :
    ∫ (x : G'), g x * f xμ' = ∫ (x : G' Γ'), g x * QuotientAddGroup.automorphize f xMeasureTheory.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.