Theorems · Theorem · measure theory

MeasureTheory.Measure.integral_isAddLeftInvariant_isAddRightInvariant_combo

∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [BorelSpace G] {μ ν : MeasureTheory.Measure G}
  [MeasureTheory.IsFiniteMeasureOnCompacts μ] [MeasureTheory.IsFiniteMeasureOnCompacts ν] [μ.IsAddLeftInvariant]
  [ν.IsAddRightInvariant] [ν.IsOpenPosMeasure] {f g : G → ℝ},
  Continuous f →
    HasCompactSupport f →
      Continuous g →
        HasCompactSupport g →
          0 ≤ g →
            ∀ {x₀ : G},
              g x₀ ≠ 0 → ∫ (x : G), f x ∂μ = (∫ (y : G), f y * (∫ (z : G), g (-z + y) ∂ν)⁻¹ ∂ν) * ∫ (x : G), g x ∂μ

In an additive group with a left invariant measure μ and a right invariant measure ν, one can express integrals with respect to μ as integrals with respect to ν up to a constant scaling factor (given in the statement as ∫ x, g x ∂μ where g is a fixed reference function) and an explicit density y ↦ 1/∫ z, g (-z + y) ∂ν.

Defined in

Mathlib.MeasureTheory.Measure.Haar.Unique

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceAddGroupIsTopologicalAddGroupMeasurableSpaceBorelSpaceMeasureTheory.IsFiniteMeasureOnCompactsMeasureTheory.IsFiniteMeasureOnCompactsMeasureTheory.Measure.IsAddLeftInvariantMeasureTheory.Measure.IsAddRightInvariantMeasureTheory.Measure.IsOpenPosMeasure