Theorems · Theorem · abstract harmonic analysis

MeasureTheory.integrable_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]
  {f : ℝ → E} {g : ℝ → E'} {μ ν : MeasureTheory.Measure ℝ} [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν]
  [μ.IsAddRightInvariant] [MeasureTheory.NullSingletonClass ν],
  MeasureTheory.IntegrableOn f (Set.Ioi 0) ν →
    MeasureTheory.IntegrableOn g (Set.Ioi 0) μ →
      ∀ (L : E →L[ℝ] E' →L[ℝ] F), MeasureTheory.Integrable (MeasureTheory.posConvolution f g L ν) μ

Defined in

Mathlib.Analysis.Convolution

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedAddCommGroupNormedAddCommGroupNormedSpaceNormedSpaceNormedSpaceMeasureTheory.SFiniteMeasureTheory.SFiniteMeasureTheory.Measure.IsAddRightInvariantMeasureTheory.NullSingletonClass