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 off
andg
w.r.t. the measureμ
.MeasureTheory.lconvolution f g μ x = (f ⋆ₗ[μ] g) x = ∫⁻ y, (f y) * (g (-y + x)) ∂μ
is the additive convolution off
andg
w.r.t. the measureμ
.
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
- MeasureTheory.«term_⋆ₗ_» = Lean.ParserDescr.trailingNode `MeasureTheory.«term_⋆ₗ_» 67 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⋆ₗ ") (Lean.ParserDescr.cat `term 66))
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
- MeasureTheory.«term_⋆ₗ__1» = Lean.ParserDescr.trailingNode `MeasureTheory.«term_⋆ₗ__1» 67 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⋆ₗ ") (Lean.ParserDescr.cat `term 66))
Instances For
Convolution of the zero function with a function returns the zero function.
Convolution of the zero function with a function returns the zero function.
Convolution of a function with the zero function returns the zero function.
Convolution of a function with the zero function returns the zero function.
The convolution of measurable functions is measurable.
The convolution of measurable functions is measurable.