Theorems · Theorem · measure theory

QuotientAddGroup.integral_eq_integral_automorphize

∀ {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 ⧸ Γ)] {E : Type u_2}
      [inst_8 : NormedAddCommGroup E] [inst_9 : NormedSpace ℝ E] [μ.IsAddRightInvariant] {f : G → E},
      MeasureTheory.Integrable f μ →
        MeasureTheory.AEStronglyMeasurable (QuotientAddGroup.automorphize f)
            (MeasureTheory.Measure.map QuotientAddGroup.mk (μ.restrict 𝓕)) →
          ∫ (x : G), f x ∂μ =
            ∫ (x : G ⧸ Γ),
              QuotientAddGroup.automorphize f x ∂MeasureTheory.Measure.map QuotientAddGroup.mk (μ.restrict 𝓕)

This is a simple version of the Unfolding Trick: Given a subgroup Γ of an additive group G, the integral of a function f on G with respect to a right-invariant measure μ is equal to the integral over the quotient G ⧸ Γ of the automorphization of f.

Defined in

Mathlib.MeasureTheory.Measure.Haar.Quotient

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddGroupMeasurableSpaceTopologicalSpaceIsTopologicalAddGroupBorelSpaceCountableMeasurableSpaceBorelSpaceNormedAddCommGroupNormedSpaceMeasureTheory.Measure.IsAddRightInvariant