Theorems · Definition · abstract harmonic analysis

MeasureTheory.convolution

{𝕜 : Type u𝕜} →
  {G : Type uG} →
    {E : Type uE} →
      {E' : Type uE'} →
        {F : Type uF} →
          [inst : NormedAddCommGroup E] →
            [inst_1 : NormedAddCommGroup E'] →
              [inst_2 : NormedAddCommGroup F] →
                [inst_3 : NontriviallyNormedField 𝕜] →
                  [inst_4 : NormedSpace 𝕜 E] →
                    [inst_5 : NormedSpace 𝕜 E'] →
                      [inst_6 : NormedSpace 𝕜 F] →
                        [inst_7 : MeasurableSpace G] →
                          [NormedSpace ℝ F] →
                            [Sub G] →
                              (G → E) →
                                (G → E') →
                                  (E →L[𝕜] E' →L[𝕜] F) →
                                    autoParam (MeasureTheory.Measure G) MeasureTheory.convolution._auto_1 → G → F

The convolution of two functions f and g with respect to a continuous bilinear map L and measure μ. It is defined to be (f ⋆[L, μ] g) x = ∫ t, L (f t) (g (x - t)) ∂μ.

Defined in

Mathlib.Analysis.Convolution

Cited by

65 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedAddCommGroupNormedAddCommGroupNontriviallyNormedFieldNormedSpaceNormedSpaceNormedSpaceMeasurableSpaceNormedSpaceSub