Documentation

Mathlib.Analysis.LConvolution

Convolution of functions using the Lebesgue integral #

In this file we define and prove properties about the convolution of two functions using the Lebesgue integral.

Design Decisions #

We define the convolution of two functions using the Lebesgue integral (in the additive case) by the formula (f ⋆ₗ[μ] g) x = ∫⁻ y, (f y) * (g (-y + x)) ∂μ. This does not agree with the formula used by MeasureTheory.convolution for convolution of two functions, however it does agree when the domain of f and g is a commutative group. The main reason for this is so that (under sufficient conditions) if {μ ν π : Measure G} {f g : G → ℝ≥0∞} are such that μ = π.withDensity f, ν = π.withDensity g where π is left-invariant then (μ ∗ ν) = π.withDensity (f ⋆ₗ[π] g). If the formula in MeasureTheory.convolution was used the order of the densities would be flipped.

Main Definitions #

noncomputable def MeasureTheory.mlconvolution {G : Type u_1} {mG : MeasurableSpace G} [Mul G] [Inv G] (f g : GENNReal) (μ : Measure G) :
GENNReal

Multiplicative convolution of functions.

Equations
Instances For
    noncomputable def MeasureTheory.lconvolution {G : Type u_1} {mG : MeasurableSpace G} [Add G] [Neg G] (f g : GENNReal) (μ : Measure G) :
    GENNReal

    Additive convolution of functions

    Equations
    Instances For

      Scoped notation for the multiplicative convolution of functions with respect to a measure μ.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        Scoped notation for the multiplicative convolution of functions with respect to volume.

        Equations
        Instances For

          Scoped notation for the additive convolution of functions with respect to a measure μ.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            Scoped notation for the additive convolution of functions with respect to volume.

            Equations
            Instances For
              theorem MeasureTheory.mlconvolution_def {G : Type u_1} {mG : MeasurableSpace G} [Mul G] [Inv G] {f g : GENNReal} {μ : Measure G} {x : G} :
              mlconvolution f g μ x = ∫⁻ (y : G), f y * g (y⁻¹ * x) μ
              theorem MeasureTheory.lconvolution_def {G : Type u_1} {mG : MeasurableSpace G} [Add G] [Neg G] {f g : GENNReal} {μ : Measure G} {x : G} :
              lconvolution f g μ x = ∫⁻ (y : G), f y * g (-y + x) μ

              The definition of additive convolution of functions.

              @[simp]
              theorem MeasureTheory.zero_mlconvolution {G : Type u_1} {mG : MeasurableSpace G} [Mul G] [Inv G] (f : GENNReal) (μ : Measure G) :
              mlconvolution 0 f μ = 0

              Convolution of the zero function with a function returns the zero function.

              @[simp]
              theorem MeasureTheory.zero_lconvolution {G : Type u_1} {mG : MeasurableSpace G} [Add G] [Neg G] (f : GENNReal) (μ : Measure G) :
              lconvolution 0 f μ = 0

              Convolution of the zero function with a function returns the zero function.

              @[simp]
              theorem MeasureTheory.mlconvolution_zero {G : Type u_1} {mG : MeasurableSpace G} [Mul G] [Inv G] (f : GENNReal) (μ : Measure G) :
              mlconvolution f 0 μ = 0

              Convolution of a function with the zero function returns the zero function.

              @[simp]
              theorem MeasureTheory.lconvolution_zero {G : Type u_1} {mG : MeasurableSpace G} [Add G] [Neg G] (f : GENNReal) (μ : Measure G) :
              lconvolution f 0 μ = 0

              Convolution of a function with the zero function returns the zero function.

              theorem MeasureTheory.measurable_mlconvolution {G : Type u_1} {mG : MeasurableSpace G} [Mul G] [Inv G] [MeasurableMul₂ G] [MeasurableInv G] {f g : GENNReal} (μ : Measure G) [SFinite μ] (hf : Measurable f) (hg : Measurable g) :

              The convolution of measurable functions is measurable.

              theorem MeasureTheory.measurable_lconvolution {G : Type u_1} {mG : MeasurableSpace G} [Add G] [Neg G] [MeasurableAdd₂ G] [MeasurableNeg G] {f g : GENNReal} (μ : Measure G) [SFinite μ] (hf : Measurable f) (hg : Measurable g) :

              The convolution of measurable functions is measurable.