Theorems · Theorem · abstract harmonic analysis

MeasureTheory.posConvolution_eq_convolution_indicator

∀ {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') (L : E →L[ℝ] E' →L[ℝ] F)
  (ν : autoParam (MeasureTheory.Measure ℝ) MeasureTheory.posConvolution_eq_convolution_indicator._auto_1)
  [MeasureTheory.NullSingletonClass ν],
  MeasureTheory.posConvolution f g L ν =
    MeasureTheory.convolution ((Set.Ioi 0).indicator f) ((Set.Ioi 0).indicator g) L ν

Defined in

Mathlib.Analysis.Convolution

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedAddCommGroupNormedAddCommGroupNormedSpaceNormedSpaceNormedSpaceMeasureTheory.NullSingletonClass