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

• MeasureTheory.mlconvolution f g μ x = (f ⋆ₘₗ[μ] g) x = ∫⁻ y, (f y) * (g (y⁻¹ * x)) ∂μ is the multiplicative convolution of f and g w.r.t. the measure μ.
• MeasureTheory.lconvolution f g μ x = (f ⋆ₗ[μ] g) x = ∫⁻ y, (f y) * (g (-y + x)) ∂μ is the additive convolution of f and g w.r.t. the measure μ.

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

Multiplicative convolution of functions.

noncomputable def MeasureTheory.lconvolution {G : Type u_1} {mG : MeasurableSpace G} [Add G] [Neg G] (f g : G → ENNReal) (μ : Measure G) : G → ENNReal

Additive convolution of functions

def MeasureTheory.«term_⋆ₘₗ[_]_» : Lean.TrailingParserDescr

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

def MeasureTheory.«term_⋆ₘₗ_» : Lean.TrailingParserDescr

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

def MeasureTheory.«term_⋆ₗ[_]_» : Lean.TrailingParserDescr

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

def MeasureTheory.«term_⋆ₗ_» : Lean.TrailingParserDescr

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

theorem MeasureTheory.mlconvolution_def {G : Type u_1} {mG : MeasurableSpace G} [Mul G] [Inv G] {f g : G → ENNReal} {μ : 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 : G → ENNReal} {μ : 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 : G → ENNReal) (μ : 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 : G → ENNReal) (μ : 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 : G → ENNReal) (μ : 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 : G → ENNReal) (μ : 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 : G → ENNReal} (μ : Measure G) [SFinite μ] (hf : Measurable f) (hg : Measurable g) : Measurable (mlconvolution f 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 : G → ENNReal} (μ : Measure G) [SFinite μ] (hf : Measurable f) (hg : Measurable g) : Measurable (lconvolution f g μ)

The convolution of measurable functions is measurable.

theorem MeasureTheory.aemeasurable_mlconvolution {G : Type u_1} {mG : MeasurableSpace G} [Group G] [MeasurableMul₂ G] [MeasurableInv G] {μ : Measure G} [μ.IsMulLeftInvariant] [SFinite μ] {f g : G → ENNReal} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) : AEMeasurable (mlconvolution f g μ) μ

The convolution of AEMeasurable functions is AEMeasurable.

theorem MeasureTheory.aemeasurable_lconvolution {G : Type u_1} {mG : MeasurableSpace G} [AddGroup G] [MeasurableAdd₂ G] [MeasurableNeg G] {μ : Measure G} [μ.IsAddLeftInvariant] [SFinite μ] {f g : G → ENNReal} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) : AEMeasurable (lconvolution f g μ) μ

The convolution of AEMeasurable functions is AEMeasurable.

theorem MeasureTheory.mlconvolution_assoc₀ {G : Type u_1} {mG : MeasurableSpace G} [Group G] [MeasurableMul₂ G] [MeasurableInv G] {μ : Measure G} [μ.IsMulLeftInvariant] [SFinite μ] {f g k : G → ENNReal} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) (hk : AEMeasurable k μ) : mlconvolution f (mlconvolution g k μ) μ = mlconvolution (mlconvolution f g μ) k μ

theorem MeasureTheory.lconvolution_assoc₀ {G : Type u_1} {mG : MeasurableSpace G} [AddGroup G] [MeasurableAdd₂ G] [MeasurableNeg G] {μ : Measure G} [μ.IsAddLeftInvariant] [SFinite μ] {f g k : G → ENNReal} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) (hk : AEMeasurable k μ) : lconvolution f (lconvolution g k μ) μ = lconvolution (lconvolution f g μ) k μ

theorem MeasureTheory.mlconvolution_assoc {G : Type u_1} {mG : MeasurableSpace G} [Group G] [MeasurableMul₂ G] [MeasurableInv G] {μ : Measure G} [μ.IsMulLeftInvariant] [SFinite μ] {f g k : G → ENNReal} (hf : Measurable f) (hg : Measurable g) (hk : Measurable k) : mlconvolution f (mlconvolution g k μ) μ = mlconvolution (mlconvolution f g μ) k μ

theorem MeasureTheory.lconvolution_assoc {G : Type u_1} {mG : MeasurableSpace G} [AddGroup G] [MeasurableAdd₂ G] [MeasurableNeg G] {μ : Measure G} [μ.IsAddLeftInvariant] [SFinite μ] {f g k : G → ENNReal} (hf : Measurable f) (hg : Measurable g) (hk : Measurable k) : lconvolution f (lconvolution g k μ) μ = lconvolution (lconvolution f g μ) k μ

Convolution is associative.

theorem MeasureTheory.mlconvolution_comm {G : Type u_1} {mG : MeasurableSpace G} [CommGroup G] [MeasurableMul₂ G] [MeasurableInv G] {μ : Measure G} [μ.IsMulLeftInvariant] [μ.IsInvInvariant] {f g : G → ENNReal} : mlconvolution f g μ = mlconvolution g f μ

Convolution is commutative when the group is commutative.

theorem MeasureTheory.lconvolution_comm {G : Type u_1} {mG : MeasurableSpace G} [AddCommGroup G] [MeasurableAdd₂ G] [MeasurableNeg G] {μ : Measure G} [μ.IsAddLeftInvariant] [μ.IsNegInvariant] {f g : G → ENNReal} : lconvolution f g μ = lconvolution g f μ

Convolution is commutative when the group is commutative.