Theorems · Theorem · measure theory

measurePreserving_quotientAddGroup_mk_of_AddQuotientMeasureEqMeasurePreimage

∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : MeasurableSpace G] (ν : MeasureTheory.Measure G) {Γ : AddSubgroup G}
  {𝓕 : Set G},
  MeasureTheory.IsAddFundamentalDomain (↥Γ.op) 𝓕 ν →
    ∀ (μ : MeasureTheory.Measure (G ⧸ Γ)) [MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ],
      MeasureTheory.MeasurePreserving QuotientAddGroup.mk (ν.restrict 𝓕) μ

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

Defined in

Mathlib.MeasureTheory.Measure.Haar.Quotient

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddGroupMeasurableSpaceMeasureTheory.AddQuotientMeasureEqMeasurePreimage