Theorems · Theorem · measure theory

MeasureTheory.integrable_mconv_iff

∀ {M : Type u_1} {F : Type u_2} [inst : Monoid M] {mM : MeasurableSpace M} [MeasurableMul₂ M]
  [inst_2 : NormedAddCommGroup F] {μ ν : MeasureTheory.Measure M} {f : M → F} [MeasureTheory.SFinite ν],
  MeasureTheory.AEStronglyMeasurable f (μ.mconv ν) →
    (MeasureTheory.Integrable f (μ.mconv ν) ↔
      (∀ᵐ (x : M) ∂μ, MeasureTheory.Integrable (fun y => f (x * y)) ν) ∧
        MeasureTheory.Integrable (fun x => ∫ (y : M), ‖f (x * y)‖ ∂ν) μ)

Defined in

Mathlib.MeasureTheory.Group.IntegralConvolution

Cited by

0 results in Mathlib

Foundations

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

Assumes

MonoidMeasurableMul₂NormedAddCommGroupMeasureTheory.SFinite