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ᵃᵒᵖ) (hγ : γ ∈ AddSubgroup.op Γ), motive { val := γ, property := hγ }) → 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 : 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 ⧸ Γ) => ↑‖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 ↥Γ'] [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 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.