Theorems · Theorem · measure theory

measurePreserving_quotientGroup_mk_of_QuotientMeasureEqMeasurePreimage

∀ {G : Type u_1} [inst : Group G] [inst_1 : MeasurableSpace G] (ν : MeasureTheory.Measure G) {Γ : Subgroup G}
  {𝓕 : Set G},
  MeasureTheory.IsFundamentalDomain (↥Γ.op) 𝓕 ν →
    ∀ (μ : MeasureTheory.Measure (G ⧸ Γ)) [MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ],
      MeasureTheory.MeasurePreserving QuotientGroup.mk (ν.restrict 𝓕) μ

Given a subgroup Γ of a topological group G with measure ν, and a measure 'μ' on the quotient G ⧸ Γ satisfying QuotientMeasureEqMeasurePreimage, the restriction of ν to a fundamental domain is measure-preserving with respect to μ.

Defined in

Mathlib.MeasureTheory.Measure.Haar.Quotient

Cited by

0 results in Mathlib

Foundations

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

Assumes

GroupMeasurableSpaceMeasureTheory.QuotientMeasureEqMeasurePreimage