Theorems · Theorem · measure theory

MeasureTheory.integral_conv

∀ {M : Type u_1} {F : Type u_2} [inst : AddMonoid M] {mM : MeasurableSpace M} [MeasurableAdd₂ M]
  [inst_2 : NormedAddCommGroup F] {μ ν : MeasureTheory.Measure M} {f : M → F} [inst_3 : NormedSpace ℝ F]
  [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν],
  MeasureTheory.Integrable f (μ.conv ν) → ∫ (x : M), f x ∂μ.conv ν = ∫ (x : M), ∫ (y : M), f (x + y) ∂ν ∂μ

Defined in

Mathlib.MeasureTheory.Group.IntegralConvolution

Cited by

3 results in Mathlib

Foundations

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

Assumes

AddMonoidMeasurableAdd₂NormedAddCommGroupNormedSpaceMeasureTheory.SFiniteMeasureTheory.SFinite