Theorems · Theorem · abstract harmonic analysis

MeasureTheory.integral_posConvolution

∀ {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup E']
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ E'] [inst_5 : NormedSpace ℝ F]
  [CompleteSpace E] [CompleteSpace E'] [CompleteSpace F] {μ ν : MeasureTheory.Measure ℝ} [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν] [μ.IsAddRightInvariant] [MeasureTheory.NullSingletonClass ν] {f : ℝ → E} {g : ℝ → E'},
  MeasureTheory.IntegrableOn f (Set.Ioi 0) ν →
    MeasureTheory.IntegrableOn g (Set.Ioi 0) μ →
      ∀ (L : E →L[ℝ] E' →L[ℝ] F),
        ∫ (x : ℝ) in Set.Ioi 0, ∫ (t : ℝ) in 0..x, (L (f t)) (g (x - t)) ∂ν ∂μ =
          (L (∫ (x : ℝ) in Set.Ioi 0, f x ∂ν)) (∫ (x : ℝ) in Set.Ioi 0, g x ∂μ)

The integral over Ioi 0 of a forward convolution of two functions is equal to the product of their integrals over this set. (Compare integral_convolution for the two-sided convolution.)

Defined in

Mathlib.Analysis.Convolution

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedAddCommGroupNormedAddCommGroupNormedSpaceNormedSpaceNormedSpaceCompleteSpaceCompleteSpaceCompleteSpaceMeasureTheory.SFiniteMeasureTheory.SFiniteMeasureTheory.Measure.IsAddRightInvariantMeasureTheory.NullSingletonClass