Convolution of functions #
This file defines the convolution on two functions, i.e. x ↦ ∫ f(t)g(x - t) ∂t
.
In the general case, these functions can be vector-valued, and have an arbitrary (additive)
group as domain. We use a continuous bilinear operation L
on these function values as
"multiplication". The domain must be equipped with a Haar measure μ
(though many individual results have weaker conditions on μ
).
For many applications we can take L = ContinuousLinearMap.lsmul ℝ ℝ
or
L = ContinuousLinearMap.mul ℝ ℝ
.
We also define ConvolutionExists
and ConvolutionExistsAt
to state that the convolution is
well-defined (everywhere or at a single point). These conditions are needed for pointwise
computations (e.g. ConvolutionExistsAt.distrib_add
), but are generally not strong enough for any
local (or global) properties of the convolution. For this we need stronger assumptions on f
and/or g
, and generally if we impose stronger conditions on one of the functions, we can impose
weaker conditions on the other.
We have proven many of the properties of the convolution assuming one of these functions
has compact support (in which case the other function only needs to be locally integrable).
We still need to prove the properties for other pairs of conditions (e.g. both functions are
rapidly decreasing)
Design Decisions #
We use a bilinear map L
to "multiply" the two functions in the integrand.
This generality has several advantages
- This allows us to compute the total derivative of the convolution, in case the functions are
multivariate. The total derivative is again a convolution, but where the codomains of the
functions can be higher-dimensional. See
HasCompactSupport.hasFDerivAt_convolution_right
. - This allows us to use
@[to_additive]
everywhere (which would not be possible if we would usemul
/smul
in the integral, since@[to_additive]
will incorrectly also try to additivize those definitions). - We need to support the case where at least one of the functions is vector-valued, but if we use
smul
to multiply the functions, that would be an asymmetric definition.
Main Definitions #
MeasureTheory.convolution f g L μ x = (f ⋆[L, μ] g) x = ∫ t, L (f t) (g (x - t)) ∂μ
is the convolution off
andg
w.r.t. the continuous bilinear mapL
and measureμ
.MeasureTheory.ConvolutionExistsAt f g x L μ
states that the convolution(f ⋆[L, μ] g) x
is well-defined (i.e. the integral exists).MeasureTheory.ConvolutionExists f g L μ
states that the convolutionf ⋆[L, μ] g
is well-defined at each point.
Main Results #
HasCompactSupport.hasFDerivAt_convolution_right
andHasCompactSupport.hasFDerivAt_convolution_left
: we can compute the total derivative of the convolution as a convolution with the total derivative of the right (left) function.HasCompactSupport.contDiff_convolution_right
andHasCompactSupport.contDiff_convolution_left
: the convolution is𝒞ⁿ
if one of the functions is𝒞ⁿ
with compact support and the other function in locally integrable.
Versions of these statements for functions depending on a parameter are also given.
MeasureTheory.convolution_tendsto_right
: Given a sequence of nonnegative normalized functions whose support tends to a small neighborhood around0
, the convolution tends to the right argument. This is specialized to bump functions inContDiffBump.convolution_tendsto_right
.
Notation #
The following notations are localized in the locale Convolution
:
f ⋆[L, μ] g
for the convolution. Note: you have to use parentheses to apply the convolution to an argument:(f ⋆[L, μ] g) x
.f ⋆[L] g := f ⋆[L, volume] g
f ⋆ g := f ⋆[lsmul ℝ ℝ] g
To do #
- Existence and (uniform) continuity of the convolution if
one of the maps is in
ℒ^p
and the other inℒ^q
with1 / p + 1 / q = 1
. This might require a generalization ofMeasureTheory.Memℒp.smul
wheresmul
is generalized to a continuous bilinear map. (see e.g. Fremlin, Measure Theory (volume 2), 255K) - The convolution is an
AEStronglyMeasurable
function (see e.g. Fremlin, Measure Theory (volume 2), 255I). - Prove properties about the convolution if both functions are rapidly decreasing.
- Use
@[to_additive]
everywhere (this likely requires changes into_additive
)
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.
Equations
- MeasureTheory.ConvolutionExistsAt f g x L μ = MeasureTheory.Integrable (fun (t : G) => (L (f t)) (g (x - t))) μ
Instances For
The convolution of f
and g
exists when the function t ↦ L (f t) (g (x - t))
is integrable
for all x : G
. There are various conditions on f
and g
to prove this.
Equations
- MeasureTheory.ConvolutionExists f g L μ = ∀ (x : G), MeasureTheory.ConvolutionExistsAt f g x L μ
Instances For
A sufficient condition to prove that f ⋆[L, μ] g
exists.
We assume that f
is integrable on a set s
and g
is bounded and ae strongly measurable
on x₀ - s
(note that both properties hold if g
is continuous with compact support).
If ‖f‖ *[μ] ‖g‖
exists, then f *[L, μ] g
exists.
If ‖f‖ *[μ] ‖g‖
exists, then f *[L, μ] g
exists.
A sufficient condition to prove that f ⋆[L, μ] g
exists.
We assume that the integrand has compact support and g
is bounded on this support (note that
both properties hold if g
is continuous with compact support). We also require that f
is
integrable on the support of the integrand, and that both functions are strongly measurable.
This is a variant of BddAbove.convolutionExistsAt'
in an abelian group with a left-invariant
measure. This allows us to state the boundedness and measurability of g
in a more natural way.
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)) ∂μ
.
Equations
- MeasureTheory.convolution f g L μ x = ∫ (t : G), (L (f t)) (g (x - t)) ∂μ
Instances For
The convolution of two functions with respect to a bilinear operation L
and a measure μ
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The convolution of two functions with respect to a bilinear operation L
and the volume.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The convolution of two real-valued functions with respect to volume.
Equations
- Convolution.«term_⋆_» = Lean.ParserDescr.trailingNode `Convolution.term_⋆_ 67 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⋆ ") (Lean.ParserDescr.cat `term 66))
Instances For
The definition of convolution where the bilinear operator is scalar multiplication. Note: it often helps the elaborator to give the type of the convolution explicitly.
The definition of convolution where the bilinear operator is multiplication.
The convolution f * g
is continuous if f
is locally integrable and g
is continuous and
compactly supported. Version where g
depends on an additional parameter in a subset s
of
a parameter space P
(and the compact support k
is independent of the parameter in s
).
The convolution f * g
is continuous if f
is locally integrable and g
is continuous and
compactly supported. Version where g
depends on an additional parameter in an open subset s
of
a parameter space P
(and the compact support k
is independent of the parameter in s
),
given in terms of compositions with an additional continuous map.
The convolution is continuous if one function is locally integrable and the other has compact support and is continuous.
The convolution is continuous if one function is integrable and the other is bounded and continuous.
Commutativity of convolution
The symmetric definition of convolution.
The symmetric definition of convolution where the bilinear operator is scalar multiplication.
The symmetric definition of convolution where the bilinear operator is multiplication.
The convolution of two even functions is also even.
Compute (f ⋆ g) x₀
if the support of the f
is within Metric.ball 0 R
, and g
is constant
on Metric.ball x₀ R
.
We can simplify the RHS further if we assume f
is integrable, but also if L = (•)
or more
generally if L
has an AntilipschitzWith
-condition.
Approximate (f ⋆ g) x₀
if the support of the f
is bounded within a ball, and g
is near
g x₀
on a ball with the same radius around x₀
. See dist_convolution_le
for a special case.
We can simplify the second argument of dist
further if we add some extra type-classes on E
and 𝕜
or if L
is scalar multiplication.
Approximate f ⋆ g
if the support of the f
is bounded within a ball, and g
is near g x₀
on a ball with the same radius around x₀
.
This is a special case of dist_convolution_le'
where L
is (•)
, f
has integral 1 and f
is
nonnegative.
(φ i ⋆ g i) (k i)
tends to z₀
as i
tends to some filter l
if
φ
is a sequence of nonnegative functions with integral1
asi
tends tol
;- The support of
φ
tends to small neighborhoods around(0 : G)
asi
tends tol
; g i
ismu
-a.e. strongly measurable asi
tends tol
;g i x
tends toz₀
as(i, x)
tends tol ×ˢ 𝓝 x₀
;k i
tends tox₀
.
See also ContDiffBump.convolution_tendsto_right
.
Convolution is associative. This has a weak but inconvenient integrability condition.
See also MeasureTheory.convolution_assoc
.
Convolution is associative. This requires that
- all maps are a.e. strongly measurable w.r.t one of the measures
f ⋆[L, ν] g
exists almost everywhere‖g‖ ⋆[μ] ‖k‖
exists almost everywhere‖f‖ ⋆[ν] (‖g‖ ⋆[μ] ‖k‖)
exists atx₀
Compute the total derivative of f ⋆ g
if g
is C^1
with compact support and f
is locally
integrable. To write down the total derivative as a convolution, we use
ContinuousLinearMap.precompR
.
The one-variable case
The derivative of the convolution f * g
is given by f * Dg
, when f
is locally integrable
and g
is C^1
and compactly supported. Version where g
depends on an additional parameter in an
open subset s
of a parameter space P
(and the compact support k
is independent of the
parameter in s
).
The convolution f * g
is C^n
when f
is locally integrable and g
is C^n
and compactly
supported. Version where g
depends on an additional parameter in an open subset s
of a
parameter space P
(and the compact support k
is independent of the parameter in s
).
In this version, all the types belong to the same universe (to get an induction working in the
proof). Use instead contDiffOn_convolution_right_with_param
, which removes this restriction.
The convolution f * g
is C^n
when f
is locally integrable and g
is C^n
and compactly
supported. Version where g
depends on an additional parameter in an open subset s
of a
parameter space P
(and the compact support k
is independent of the parameter in s
).
The convolution f * g
is C^n
when f
is locally integrable and g
is C^n
and compactly
supported. Version where g
depends on an additional parameter in an open subset s
of a
parameter space P
(and the compact support k
is independent of the parameter in s
),
given in terms of composition with an additional smooth function.
The convolution g * f
is C^n
when f
is locally integrable and g
is C^n
and compactly
supported. Version where g
depends on an additional parameter in an open subset s
of a
parameter space P
(and the compact support k
is independent of the parameter in s
).
The convolution g * f
is C^n
when f
is locally integrable and g
is C^n
and compactly
supported. Version where g
depends on an additional parameter in an open subset s
of a
parameter space P
(and the compact support k
is independent of the parameter in s
),
given in terms of composition with additional smooth functions.
The forward convolution of two functions f
and g
on ℝ
, with respect to a continuous
bilinear map L
and measure ν
. It is defined to be the function mapping x
to
∫ t in 0..x, L (f t) (g (x - t)) ∂ν
if 0 < x
, and 0 otherwise.
Equations
Instances For
The integral over Ioi 0
of a forward convolution of two functions is equal to the product
of their integrals over this set. (Compare integral_convolution
for the two-sided convolution.)