Theorems · Theorem · measure theory

MeasureTheory.IsAddFundamentalDomain.absolutelyContinuous_map

∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : MeasurableSpace G] [inst_2 : TopologicalSpace G]
  [IsTopologicalAddGroup G] [BorelSpace G] {μ : MeasureTheory.Measure G} {Γ : AddSubgroup G} {𝓕 : Set G},
  MeasureTheory.IsAddFundamentalDomain (↥Γ.op) 𝓕 μ →
    ∀ [Countable ↥Γ] [inst_6 : MeasurableSpace (G ⧸ Γ)] [BorelSpace (G ⧸ Γ)] [μ.IsAddRightInvariant],
      (MeasureTheory.Measure.map QuotientAddGroup.mk μ).AbsolutelyContinuous
        (MeasureTheory.Measure.map QuotientAddGroup.mk (μ.restrict 𝓕))

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!

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

AddGroupMeasurableSpaceTopologicalSpaceIsTopologicalAddGroupBorelSpaceCountableMeasurableSpaceBorelSpaceMeasureTheory.Measure.IsAddRightInvariant