Theorems · Definition · abstract harmonic analysis

MeasureTheory.ConvolutionExistsAt

{𝕜 : 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] →
                          [Sub G] →
                            (G → E) →
                              (G → E') →
                                G →
                                  (E →L[𝕜] E' →L[𝕜] F) →
                                    autoParam (MeasureTheory.Measure G) MeasureTheory.ConvolutionExistsAt._auto_1 → Prop

The convolution of f and g exists at x when the function t ↦ L (f t) (g (x - t)) is integrable. There are various conditions on f and g to prove this.

Defined in

Mathlib.Analysis.Convolution

Cited by

18 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedAddCommGroupNormedAddCommGroupNontriviallyNormedFieldNormedSpaceNormedSpaceNormedSpaceMeasurableSpaceSub