Theorems · Theorem · measure theory

MeasureTheory.IsAddFundamentalDomain.addQuotientMeasureEqMeasurePreimage

∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α]
  {ν : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α ν] [Countable G] [MeasurableConstVAdd G α]
  {μ : MeasureTheory.Measure (Quotient (AddAction.orbitRel G α))} {s : Set α},
  MeasureTheory.IsAddFundamentalDomain G s ν →
    μ = MeasureTheory.Measure.map (Quotient.mk (AddAction.orbitRel G α)) (ν.restrict s) →
      MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ

One can prove AddQuotientMeasureEqMeasurePreimage by checking behavior with respect to a single additive fundamental domain.

Defined in

Mathlib.MeasureTheory.Group.FundamentalDomain

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddGroupAddActionMeasurableSpaceMeasureTheory.VAddInvariantMeasureCountableMeasurableConstVAdd