Theorems · Theorem · abstract harmonic analysis

MeasureTheory.Measure.lintegral_mconv

∀ {M : Type u_1} [inst : Monoid M] [inst_1 : MeasurableSpace M] [MeasurableMul₂ M] {μ ν : MeasureTheory.Measure M}
  [MeasureTheory.SFinite ν] {f : M → ENNReal},
  Measurable f → ∫⁻ (z : M), f z ∂μ.mconv ν = ∫⁻ (x : M), ∫⁻ (y : M), f (x * y) ∂ν ∂μ

Defined in

Mathlib.MeasureTheory.Group.Convolution

Cited by

2 results in Mathlib

Foundations

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

Assumes

MonoidMeasurableSpaceMeasurableMul₂MeasureTheory.SFinite