Theorems · Theorem · measure theory

MeasureTheory.measure_add_lintegral_eq

∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd₂ G] (μ ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] {s : Set G} [MeasurableNeg G] [μ.IsAddLeftInvariant]
  [ν.IsAddLeftInvariant],
  MeasurableSet s →
    ∀ (f : G → ENNReal), Measurable f → μ s * ∫⁻ (y : G), f y ∂ν = ∫⁻ (x : G), ν ((fun z => z + x) ⁻¹' s) * f (-x) ∂μ

This is the computation performed in the proof of [Halmos, §60 Th. A].

Defined in

Mathlib.MeasureTheory.Group.Prod

Cited by

3 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceAddGroupMeasurableAdd₂MeasureTheory.SFiniteMeasureTheory.SFiniteMeasurableNegMeasureTheory.Measure.IsAddLeftInvariantMeasureTheory.Measure.IsAddLeftInvariant