Theorems · Theorem · measure theory

MeasureTheory.IsFundamentalDomain.absolutelyContinuous_map

∀ {G : Type u_1} [inst : Group G] [inst_1 : MeasurableSpace G] [inst_2 : TopologicalSpace G] [IsTopologicalGroup G]
  [BorelSpace G] {μ : MeasureTheory.Measure G} {Γ : Subgroup G} {𝓕 : Set G},
  MeasureTheory.IsFundamentalDomain (↥Γ.op) 𝓕 μ →
    ∀ [Countable ↥Γ] [inst_6 : MeasurableSpace (G ⧸ Γ)] [BorelSpace (G ⧸ Γ)] [μ.IsMulRightInvariant],
      (MeasureTheory.Measure.map QuotientGroup.mk μ).AbsolutelyContinuous
        (MeasureTheory.Measure.map QuotientGroup.mk (μ.restrict 𝓕))

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!

Defined in

Mathlib.MeasureTheory.Measure.Haar.Quotient

Cited by

1 results in Mathlib

Foundations

Depth 213 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupMeasurableSpaceTopologicalSpaceIsTopologicalGroupBorelSpaceCountableMeasurableSpaceBorelSpaceMeasureTheory.Measure.IsMulRightInvariant