# mathlib3documentation

analysis.convolution

# Convolution of functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 = lsmul ℝ ℝ` or `L = mul ℝ ℝ`.

We also define `convolution_exists` and `convolution_exists_at` to state that the convolution is well-defined (everywhere or at a single point). These conditions are needed for pointwise computations (e.g. `convolution_exists_at.distrib_add`), but are generally not stong 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 `has_compact_support.has_fderiv_at_convolution_right`.
• This allows us to use `@[to_additive]` everywhere (which would not be possible if we would use `mul`/`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 #

• `convolution f g L μ x = (f ⋆[L, μ] g) x = ∫ t, L (f t) (g (x - t)) ∂μ` is the convolution of `f` and `g` w.r.t. the continuous bilinear map `L` and measure `μ`.
• `convolution_exists_at f g x L μ` states that the convolution `(f ⋆[L, μ] g) x` is well-defined (i.e. the integral exists).
• `convolution_exists f g L μ` states that the convolution `f ⋆[L, μ] g` is well-defined at each point.

# Main Results #

• `has_compact_support.has_fderiv_at_convolution_right` and `has_compact_support.has_fderiv_at_convolution_left`: we can compute the total derivative of the convolution as a convolution with the total derivative of the right (left) function.
• `has_compact_support.cont_diff_convolution_right` and `has_compact_support.cont_diff_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.

• `convolution_tendsto_right`: Given a sequence of nonnegative normalized functions whose support tends to a small neighborhood around `0`, the convolution tends to the right argument. This is specialized to bump functions in `cont_diff_bump.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` with `1 / p + 1 / q = 1`. This might require a generalization of `measure_theory.mem_ℒp.smul` where `smul` is generalized to a continuous bilinear map. (see e.g. Fremlin, Measure Theory (volume 2), 255K)
• The convolution is a `ae_strongly_measurable` 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
theorem convolution_integrand_bound_right_of_le_of_subset {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} {g : G E'} [ E] [ E'] [ F] (L : E →L[𝕜] E' →L[𝕜] F) [add_group G] {C : } (hC : (i : G), g i C) {x t : G} {s u : set G} (hx : x s) (hu : + s u) :
(L (f t)) (g (x - t)) u.indicator (λ (t : G), L * f t * C) t
theorem has_compact_support.convolution_integrand_bound_right_of_subset {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} {g : G E'} [ E] [ E'] [ F] (L : E →L[𝕜] E' →L[𝕜] F) [add_group G] (hcg : has_compact_support g) (hg : continuous g) {x t : G} {s u : set G} (hx : x s) (hu : + s u) :
(L (f t)) (g (x - t)) u.indicator (λ (t : G), L * f t * (i : G), g i) t
theorem has_compact_support.convolution_integrand_bound_right {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} {g : G E'} [ E] [ E'] [ F] (L : E →L[𝕜] E' →L[𝕜] F) [add_group G] (hcg : has_compact_support g) (hg : continuous g) {x t : G} {s : set G} (hx : x s) :
(L (f t)) (g (x - t)) (- + s).indicator (λ (t : G), L * f t * (i : G), g i) t
theorem continuous.convolution_integrand_fst {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} {g : G E'} [ E] [ E'] [ F] (L : E →L[𝕜] E' →L[𝕜] F) [add_group G] (hg : continuous g) (t : G) :
continuous (λ (x : G), (L (f t)) (g (x - t)))
theorem has_compact_support.convolution_integrand_bound_left {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} {g : G E'} [ E] [ E'] [ F] (L : E →L[𝕜] E' →L[𝕜] F) [add_group G] (hcf : has_compact_support f) (hf : continuous f) {x t : G} {s : set G} (hx : x s) :
(L (f (x - t))) (g t) (- + s).indicator (λ (t : G), (L * (i : G), f i) * g t) t
def convolution_exists_at {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [ E] [ E'] [ F] [has_sub G] (f : G E) (g : G E') (x : G) (L : E →L[𝕜] E' →L[𝕜] F) (μ : . "volume_tac") :
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.

Equations
def convolution_exists {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [ E] [ E'] [ F] [has_sub G] (f : G E) (g : G E') (L : E →L[𝕜] E' →L[𝕜] F) (μ : . "volume_tac") :
Prop

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
• L μ = (x : G), L μ
theorem convolution_exists_at.integrable {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} {g : G E'} [ E] [ E'] [ F] {L : E →L[𝕜] E' →L[𝕜] F} {μ : measure_theory.measure G} [has_sub G] {x : G} (h : L μ) :
measure_theory.integrable (λ (t : G), (L (f t)) (g (x - t))) μ
theorem measure_theory.ae_strongly_measurable.convolution_integrand' {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} {g : G E'} [ E] [ E'] [ F] (L : E →L[𝕜] E' →L[𝕜] F) {μ ν : measure_theory.measure G} [add_group G] (hg : (measure_theory.measure.map (λ (p : G × G), p.fst - p.snd) (μ.prod ν))) :
measure_theory.ae_strongly_measurable (λ (p : G × G), (L (f p.snd)) (g (p.fst - p.snd))) (μ.prod ν)
theorem measure_theory.ae_strongly_measurable.convolution_integrand_snd' {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} {g : G E'} [ E] [ E'] [ F] (L : E →L[𝕜] E' →L[𝕜] F) {μ : measure_theory.measure G} [add_group G] {x : G} (hg : (measure_theory.measure.map (λ (t : G), x - t) μ)) :
measure_theory.ae_strongly_measurable (λ (t : G), (L (f t)) (g (x - t))) μ
theorem measure_theory.ae_strongly_measurable.convolution_integrand_swap_snd' {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} {g : G E'} [ E] [ E'] [ F] (L : E →L[𝕜] E' →L[𝕜] F) {μ : measure_theory.measure G} [add_group G] {x : G} (hf : (measure_theory.measure.map (λ (t : G), x - t) μ))  :
measure_theory.ae_strongly_measurable (λ (t : G), (L (f (x - t))) (g t)) μ
theorem bdd_above.convolution_exists_at' {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} {g : G E'} [ E] [ E'] [ F] (L : E →L[𝕜] E' →L[𝕜] F) {μ : measure_theory.measure G} [add_group G] {x₀ : G} {s : set G} (hbg : bdd_above ((λ (i : G), g i) '' ((λ (t : G), -t + x₀) ⁻¹' s))) (hs : measurable_set s) (h2s : function.support (λ (t : G), (L (f t)) (g (x₀ - t))) s) (hf : μ) (hmg : (measure_theory.measure.map (λ (t : G), x₀ - t) (μ.restrict s))) :
x₀ L μ

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).

theorem convolution_exists_at.of_norm' {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} {g : G E'} [ E] [ E'] [ F] (L : E →L[𝕜] E' →L[𝕜] F) {μ : measure_theory.measure G} [add_group G] {x₀ : G} (h : convolution_exists_at (λ (x : G), f x) (λ (x : G), g x) x₀ μ) (hmf : μ) (hmg : (measure_theory.measure.map (λ (t : G), x₀ - t) μ)) :
x₀ L μ

If `‖f‖ *[μ] ‖g‖` exists, then `f *[L, μ] g` exists.

theorem measure_theory.ae_strongly_measurable.convolution_integrand_snd {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} {g : G E'} [ E] [ E'] [ F] (L : E →L[𝕜] E' →L[𝕜] F) {μ : measure_theory.measure G} [add_group G] (x : G) :
measure_theory.ae_strongly_measurable (λ (t : G), (L (f t)) (g (x - t))) μ
theorem measure_theory.ae_strongly_measurable.convolution_integrand_swap_snd {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} {g : G E'} [ E] [ E'] [ F] (L : E →L[𝕜] E' →L[𝕜] F) {μ : measure_theory.measure G} [add_group G] (x : G) :
measure_theory.ae_strongly_measurable (λ (t : G), (L (f (x - t))) (g t)) μ
theorem convolution_exists_at.of_norm {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} {g : G E'} [ E] [ E'] [ F] (L : E →L[𝕜] E' →L[𝕜] F) {μ : measure_theory.measure G} [add_group G] {x₀ : G} (h : convolution_exists_at (λ (x : G), f x) (λ (x : G), g x) x₀ μ) (hmf : μ) (hmg : μ) :
x₀ L μ

If `‖f‖ *[μ] ‖g‖` exists, then `f *[L, μ] g` exists.

theorem measure_theory.ae_strongly_measurable.convolution_integrand {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} {g : G E'} [ E] [ E'] [ F] (L : E →L[𝕜] E' →L[𝕜] F) {μ ν : measure_theory.measure G} [add_group G]  :
measure_theory.ae_strongly_measurable (λ (p : G × G), (L (f p.snd)) (g (p.fst - p.snd))) (μ.prod ν)
theorem measure_theory.integrable.convolution_integrand {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} {g : G E'} [ E] [ E'] [ F] (L : E →L[𝕜] E' →L[𝕜] F) {μ ν : measure_theory.measure G} [add_group G] (hf : ν) (hg : μ) :
measure_theory.integrable (λ (p : G × G), (L (f p.snd)) (g (p.fst - p.snd))) (μ.prod ν)
theorem measure_theory.integrable.ae_convolution_exists {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} {g : G E'} [ E] [ E'] [ F] (L : E →L[𝕜] E' →L[𝕜] F) {μ ν : measure_theory.measure G} [add_group G] (hf : ν) (hg : μ) :
∀ᵐ (x : G) μ, L ν
theorem has_compact_support.convolution_exists_at {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} {g : G E'} [ E] [ E'] [ F] (L : E →L[𝕜] E' →L[𝕜] F) {μ : measure_theory.measure G} [add_group G] [borel_space G] {x₀ : G} (h : has_compact_support (λ (t : G), (L (f t)) (g (x₀ - t)))) (hf : μ) (hg : continuous g) :
x₀ L μ
theorem has_compact_support.convolution_exists_right {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} {g : G E'} [ E] [ E'] [ F] (L : E →L[𝕜] E' →L[𝕜] F) {μ : measure_theory.measure G} [add_group G] [borel_space G] (hcg : has_compact_support g) (hf : μ) (hg : continuous g) :
L μ
theorem has_compact_support.convolution_exists_left_of_continuous_right {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} {g : G E'} [ E] [ E'] [ F] (L : E →L[𝕜] E' →L[𝕜] F) {μ : measure_theory.measure G} [add_group G] [borel_space G] (hcf : has_compact_support f) (hf : μ) (hg : continuous g) :
L μ
theorem bdd_above.convolution_exists_at {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} {g : G E'} [ E] [ E'] [ F] (L : E →L[𝕜] E' →L[𝕜] F) {μ : measure_theory.measure G} {x₀ : G} {s : set G} (hbg : bdd_above ((λ (i : G), g i) '' ((λ (t : G), x₀ - t) ⁻¹' s))) (hs : measurable_set s) (h2s : function.support (λ (t : G), (L (f t)) (g (x₀ - t))) s) (hf : μ) (hmg : μ) :
x₀ L μ

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 `bdd_above.convolution_exists_at'` 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.

theorem convolution_exists_at_flip {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} {g : G E'} {x : G} [ E] [ E'] [ F] {L : E →L[𝕜] E' →L[𝕜] F} {μ : measure_theory.measure G} [μ.is_neg_invariant] :
L.flip μ L μ
theorem convolution_exists_at.integrable_swap {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} {g : G E'} {x : G} [ E] [ E'] [ F] {L : E →L[𝕜] E' →L[𝕜] F} {μ : measure_theory.measure G} [μ.is_neg_invariant] (h : L μ) :
measure_theory.integrable (λ (t : G), (L (f (x - t))) (g t)) μ
theorem convolution_exists_at_iff_integrable_swap {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} {g : G E'} {x : G} [ E] [ E'] [ F] {L : E →L[𝕜] E' →L[𝕜] F} {μ : measure_theory.measure G} [μ.is_neg_invariant] :
L μ measure_theory.integrable (λ (t : G), (L (f (x - t))) (g t)) μ
theorem has_compact_support.convolution_exists_left {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} {g : G E'} [ E] [ E'] [ F] (L : E →L[𝕜] E' →L[𝕜] F) {μ : measure_theory.measure G} [borel_space G] [μ.is_neg_invariant] (hcf : has_compact_support f) (hf : continuous f) (hg : μ) :
L μ
theorem has_compact_support.convolution_exists_right_of_continuous_left {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} {g : G E'} [ E] [ E'] [ F] (L : E →L[𝕜] E' →L[𝕜] F) {μ : measure_theory.measure G} [borel_space G] [μ.is_neg_invariant] (hcg : has_compact_support g) (hf : continuous f) (hg : μ) :
L μ
noncomputable def convolution {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [ E] [ E'] [ F] [ F] [has_sub G] (f : G E) (g : G E') (L : E →L[𝕜] E' →L[𝕜] F) (μ : . "volume_tac") :
G F

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
theorem convolution_def {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} {g : G E'} {x : G} [ E] [ E'] [ F] (L : E →L[𝕜] E' →L[𝕜] F) {μ : measure_theory.measure G} [ F] [has_sub G] :
g L μ x = (t : G), (L (f t)) (g (x - t)) μ
theorem convolution_lsmul {𝕜 : Type u𝕜} {G : Type uG} {F : Type uF} {x : G} [ F] {μ : measure_theory.measure G} [ F] [has_sub G] {f : G 𝕜} {g : G F} :
g μ x = (t : G), f t g (x - t) μ

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.

theorem convolution_mul {𝕜 : Type u𝕜} {G : Type uG} {x : G} {μ : measure_theory.measure G} [has_sub G] [ 𝕜] {f g : G 𝕜} :
g μ x = (t : G), f t * g (x - t) μ

The definition of convolution where the bilinear operator is multiplication.

theorem smul_convolution {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} {g : G E'} [ E] [ E'] [ F] {L : E →L[𝕜] E' →L[𝕜] F} {μ : measure_theory.measure G} [ F] [add_group G] [ F] {y : 𝕜} :
convolution (y f) g L μ = y g L μ
theorem convolution_smul {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} {g : G E'} [ E] [ E'] [ F] {L : E →L[𝕜] E' →L[𝕜] F} {μ : measure_theory.measure G} [ F] [add_group G] [ F] {y : 𝕜} :
(y g) L μ = y g L μ
@[simp]
theorem zero_convolution {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {g : G E'} [ E] [ E'] [ F] {L : E →L[𝕜] E' →L[𝕜] F} {μ : measure_theory.measure G} [ F] [add_group G] :
g L μ = 0
@[simp]
theorem convolution_zero {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} [ E] [ E'] [ F] {L : E →L[𝕜] E' →L[𝕜] F} {μ : measure_theory.measure G} [ F] [add_group G] :
0 L μ = 0
theorem convolution_exists_at.distrib_add {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} {g g' : G E'} [ E] [ E'] [ F] {L : E →L[𝕜] E' →L[𝕜] F} {μ : measure_theory.measure G} [ F] [add_group G] {x : G} (hfg : L μ) (hfg' : x L μ) :
(g + g') L μ x = g L μ x + g' L μ x
theorem convolution_exists.distrib_add {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} {g g' : G E'} [ E] [ E'] [ F] {L : E →L[𝕜] E' →L[𝕜] F} {μ : measure_theory.measure G} [ F] [add_group G] (hfg : L μ) (hfg' : L μ) :
(g + g') L μ = g L μ + g' L μ
theorem convolution_exists_at.add_distrib {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f f' : G E} {g : G E'} [ E] [ E'] [ F] {L : E →L[𝕜] E' →L[𝕜] F} {μ : measure_theory.measure G} [ F] [add_group G] {x : G} (hfg : L μ) (hfg' : x L μ) :
convolution (f + f') g L μ x = g L μ x + g L μ x
theorem convolution_exists.add_distrib {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f f' : G E} {g : G E'} [ E] [ E'] [ F] {L : E →L[𝕜] E' →L[𝕜] F} {μ : measure_theory.measure G} [ F] [add_group G] (hfg : L μ) (hfg' : L μ) :
convolution (f + f') g L μ = g L μ + g L μ
theorem convolution_mono_right {G : Type uG} {x : G} {μ : measure_theory.measure G} [add_group G] {f g g' : G } (hfg : μ) (hfg' : μ) (hf : (x : G), 0 f x) (hg : (x : G), g x g' x) :
μ x μ x
theorem convolution_mono_right_of_nonneg {G : Type uG} {x : G} {μ : measure_theory.measure G} [add_group G] {f g g' : G } (hfg' : μ) (hf : (x : G), 0 f x) (hg : (x : G), g x g' x) (hg' : (x : G), 0 g' x) :
μ x μ x
theorem convolution_congr {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f f' : G E} {g g' : G E'} [ E] [ E'] [ F] (L : E →L[𝕜] E' →L[𝕜] F) {μ : measure_theory.measure G} [ F] [add_group G] (h1 : f =ᵐ[μ] f') (h2 : g =ᵐ[μ] g') :
g L μ = g' L μ
theorem support_convolution_subset_swap {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} {g : G E'} [ E] [ E'] [ F] (L : E →L[𝕜] E' →L[𝕜] F) {μ : measure_theory.measure G} [ F] [add_group G] :
theorem measure_theory.integrable.integrable_convolution {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} {g : G E'} [ E] [ E'] [ F] (L : E →L[𝕜] E' →L[𝕜] F) {μ : measure_theory.measure G} [ F] [add_group G] (hf : μ) (hg : μ) :
theorem has_compact_support.convolution {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} {g : G E'} [ E] [ E'] [ F] (L : E →L[𝕜] E' →L[𝕜] F) {μ : measure_theory.measure G} [ F] [add_group G] [t2_space G] (hcf : has_compact_support f) (hcg : has_compact_support g) :
theorem continuous_on_convolution_right_with_param' {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {P : Type uP} {f : G E} [ E] [ E'] [ F] (L : E →L[𝕜] E' →L[𝕜] F) {μ : measure_theory.measure G} [ F] [add_group G] [borel_space G] {g : P G E'} {s : set P} {k : set G} (hk : is_compact k) (h'k : is_closed k) (hgs : (p : P) (x : G), p s x k g p x = 0) (hf : μ) (hg : (s ×ˢ set.univ)) :
continuous_on (λ (q : P × G), (g q.fst) L μ q.snd) (s ×ˢ set.univ)

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`), not assuming `t2_space G`.

theorem continuous_on_convolution_right_with_param {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {P : Type uP} {f : G E} [ E] [ E'] [ F] (L : E →L[𝕜] E' →L[𝕜] F) {μ : measure_theory.measure G} [ F] [add_group G] [borel_space G] [t2_space G] {g : P G E'} {s : set P} {k : set G} (hk : is_compact k) (hgs : (p : P) (x : G), p s x k g p x = 0) (hf : μ) (hg : (s ×ˢ set.univ)) :
continuous_on (λ (q : P × G), (g q.fst) L μ q.snd) (s ×ˢ set.univ)

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`).

theorem continuous_on_convolution_right_with_param_comp' {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {P : Type uP} {f : G E} [ E] [ E'] [ F] (L : E →L[𝕜] E' →L[𝕜] F) {μ : measure_theory.measure G} [ F] [add_group G] [borel_space G] {s : set P} {v : P G} (hv : s) {g : P G E'} {k : set G} (hk : is_compact k) (h'k : is_closed k) (hgs : (p : P) (x : G), p s x k g p x = 0) (hf : μ) (hg : (s ×ˢ set.univ)) :
continuous_on (λ (x : P), (g x) L μ (v x)) 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. Version not assuming `t2_space G`.

theorem continuous_on_convolution_right_with_param_comp {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {P : Type uP} {f : G E} [ E] [ E'] [ F] (L : E →L[𝕜] E' →L[𝕜] F) {μ : measure_theory.measure G} [ F] [add_group G] [borel_space G] [t2_space G] {s : set P} {v : P G} (hv : s) {g : P G E'} {k : set G} (hk : is_compact k) (hgs : (p : P) (x : G), p s x k g p x = 0) (hf : μ) (hg : (s ×ˢ set.univ)) :
continuous_on (λ (x : P), (g x) L μ (v x)) 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.

theorem has_compact_support.continuous_convolution_right {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} {g : G E'} [ E] [ E'] [ F] (L : E →L[𝕜] E' →L[𝕜] F) {μ : measure_theory.measure G} [ F] [add_group G] [borel_space G] (hcg : has_compact_support g) (hf : μ) (hg : continuous g) :
continuous g L μ)

The convolution is continuous if one function is locally integrable and the other has compact support and is continuous.

theorem bdd_above.continuous_convolution_right_of_integrable {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} {g : G E'} [ E] [ E'] [ F] (L : E →L[𝕜] E' →L[𝕜] F) {μ : measure_theory.measure G} [ F] [add_group G] [borel_space G] (hbg : bdd_above (set.range (λ (x : G), g x))) (hf : μ) (hg : continuous g) :
continuous g L μ)

The convolution is continuous if one function is integrable and the other is bounded and continuous.

theorem support_convolution_subset {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} {g : G E'} [ E] [ E'] [ F] (L : E →L[𝕜] E' →L[𝕜] F) {μ : measure_theory.measure G} [ F]  :
theorem convolution_flip {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} {g : G E'} [ E] [ E'] [ F] (L : E →L[𝕜] E' →L[𝕜] F) {μ : measure_theory.measure G} [ F] [μ.is_neg_invariant]  :
f L.flip μ = g L μ

Commutativity of convolution

theorem convolution_eq_swap {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} {g : G E'} {x : G} [ E] [ E'] [ F] (L : E →L[𝕜] E' →L[𝕜] F) {μ : measure_theory.measure G} [ F] [μ.is_neg_invariant]  :
g L μ x = (t : G), (L (f (x - t))) (g t) μ

The symmetric definition of convolution.

theorem convolution_lsmul_swap {𝕜 : Type u𝕜} {G : Type uG} {F : Type uF} {x : G} [ F] {μ : measure_theory.measure G} [ F] [μ.is_neg_invariant] {f : G 𝕜} {g : G F} :
g μ x = (t : G), f (x - t) g t μ

The symmetric definition of convolution where the bilinear operator is scalar multiplication.

theorem convolution_mul_swap {𝕜 : Type u𝕜} {G : Type uG} {x : G} {μ : measure_theory.measure G} [μ.is_neg_invariant] [ 𝕜] {f g : G 𝕜} :
g μ x = (t : G), f (x - t) * g t μ

The symmetric definition of convolution where the bilinear operator is multiplication.

theorem convolution_neg_of_neg_eq {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} {g : G E'} {x : G} [ E] [ E'] [ F] (L : E →L[𝕜] E' →L[𝕜] F) {μ : measure_theory.measure G} [ F] [μ.is_neg_invariant] (h1 : ∀ᵐ (x : G) μ, f (-x) = f x) (h2 : ∀ᵐ (x : G) μ, g (-x) = g x) :
g L μ (-x) = g L μ x

The convolution of two even functions is also even.

theorem has_compact_support.continuous_convolution_left {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} {g : G E'} [ E] [ E'] [ F] (L : E →L[𝕜] E' →L[𝕜] F) {μ : measure_theory.measure G} [ F] [μ.is_neg_invariant] [borel_space G] (hcf : has_compact_support f) (hf : continuous f) (hg : μ) :
continuous g L μ)
theorem bdd_above.continuous_convolution_left_of_integrable {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} {g : G E'} [ E] [ E'] [ F] (L : E →L[𝕜] E' →L[𝕜] F) {μ : measure_theory.measure G} [ F] [μ.is_neg_invariant] [borel_space G] (hbf : bdd_above (set.range (λ (x : G), f x))) (hf : continuous f) (hg : μ) :
continuous g L μ)
theorem convolution_eq_right' {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} {g : G E'} [ E] [ E'] [ F] (L : E →L[𝕜] E' →L[𝕜] F) {μ : measure_theory.measure G} [ F] {x₀ : G} {R : } (hf : R) (hg : (x : G), x R g x = g x₀) :
g L μ x₀ = (t : G), (L (f t)) (g x₀) μ

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 a `antilipschitz_with`-condition.

theorem dist_convolution_le' {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} {g : G E'} [ E] [ E'] [ F] (L : E →L[𝕜] E' →L[𝕜] F) {μ : measure_theory.measure G} [ F] [borel_space G] {x₀ : G} {R ε : } {z₀ : E'} (hε : 0 ε) (hif : μ) (hf : R) (hmg : μ) (hg : (x : G), x R has_dist.dist (g x) z₀ ε) :
has_dist.dist g L μ x₀) ( (t : G), (L (f t)) z₀ μ) L * (x : G), f x μ * ε

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.

theorem dist_convolution_le {G : Type uG} {E' : Type uE'} {g : G E'} {μ : measure_theory.measure G} [borel_space G] [ E'] [complete_space E'] {f : G } {x₀ : G} {R ε : } {z₀ : E'} (hε : 0 ε) (hf : R) (hnf : (x : G), 0 f x) (hintf : (x : G), f x μ = 1) (hmg : μ) (hg : (x : G), x R has_dist.dist (g x) z₀ ε) :
has_dist.dist μ x₀) z₀ ε

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.

theorem convolution_tendsto_right {G : Type uG} {E' : Type uE'} {μ : measure_theory.measure G} [borel_space G] [ E'] [complete_space E'] {ι : Type u_1} {g : ι G E'} {l : filter ι} {x₀ : G} {z₀ : E'} {φ : ι G } {k : ι G} (hnφ : ∀ᶠ (i : ι) in l, (x : G), 0 φ i x) (hiφ : ∀ᶠ (i : ι) in l, (x : G), φ i x μ = 1) (hφ : filter.tendsto (λ (n : ι), function.support (φ n)) l (nhds 0).small_sets) (hmg : ∀ᶠ (i : ι) in l, ) (hcg : (l.prod (nhds x₀)) (nhds z₀)) (hk : (nhds x₀)) :
filter.tendsto (λ (i : ι), convolution (φ i) (g i) μ (k i)) l (nhds z₀)

`(φ i ⋆ g i) (k i)` tends to `z₀` as `i` tends to some filter `l` if

• `φ` is a sequence of nonnegative functions with integral `1` as `i` tends to `l`;
• The support of `φ` tends to small neighborhoods around `(0 : G)` as `i` tends to `l`;
• `g i` is `mu`-a.e. strongly measurable as `i` tends to `l`;
• `g i x` tends to `z₀` as `(i, x)` tends to `l ×ᶠ 𝓝 x₀`;
• `k i` tends to `x₀`.

See also `cont_diff_bump.convolution_tendsto_right`.

theorem cont_diff_bump.convolution_eq_right {G : Type uG} {E' : Type uE'} {g : G E'} {μ : measure_theory.measure G} [ E'] [ G] [complete_space E'] {φ : cont_diff_bump 0} {x₀ : G} (hg : (x : G), x φ.R g x = g x₀) :
x₀ = g x₀

If `φ` is a bump function, compute `(φ ⋆ g) x₀` if `g` is constant on `metric.ball x₀ φ.R`.

theorem cont_diff_bump.normed_convolution_eq_right {G : Type uG} {E' : Type uE'} {g : G E'} {μ : measure_theory.measure G} [ E'] [ G] [complete_space E'] {φ : cont_diff_bump 0} [borel_space G] {x₀ : G} (hg : (x : G), x φ.R g x = g x₀) :
convolution (φ.normed μ) g μ x₀ = g x₀

If `φ` is a normed bump function, compute `φ ⋆ g` if `g` is constant on `metric.ball x₀ φ.R`.

theorem cont_diff_bump.dist_normed_convolution_le {G : Type uG} {E' : Type uE'} {g : G E'} {μ : measure_theory.measure G} [ E'] [ G] [complete_space E'] {φ : cont_diff_bump 0} [borel_space G] {x₀ : G} {ε : } (hmg : μ) (hg : (x : G), x φ.R has_dist.dist (g x) (g x₀) ε) :
has_dist.dist (convolution (φ.normed μ) g μ x₀) (g x₀) ε

If `φ` is a normed bump function, approximate `(φ ⋆ g) x₀` if `g` is near `g x₀` on a ball with radius `φ.R` around `x₀`.

theorem cont_diff_bump.convolution_tendsto_right {G : Type uG} {E' : Type uE'} {μ : measure_theory.measure G} [ E'] [ G] [complete_space E'] [borel_space G] {ι : Type u_1} {φ : ι } {g : ι G E'} {k : ι G} {x₀ : G} {z₀ : E'} {l : filter ι} (hφ : filter.tendsto (λ (i : ι), (φ i).R) l (nhds 0)) (hig : ∀ᶠ (i : ι) in l, ) (hcg : (l.prod (nhds x₀)) (nhds z₀)) (hk : (nhds x₀)) :
filter.tendsto (λ (i : ι), convolution (λ (x : G), (φ i).normed μ x) (g i) μ (k i)) l (nhds z₀)

`(φ i ⋆ g i) (k i)` tends to `z₀` as `i` tends to some filter `l` if

• `φ` is a sequence of normed bump functions such that `(φ i).R` tends to `0` as `i` tends to `l`;
• `g i` is `mu`-a.e. strongly measurable as `i` tends to `l`;
• `g i x` tends to `z₀` as `(i, x)` tends to `l ×ᶠ 𝓝 x₀`;
• `k i` tends to `x₀`.
theorem cont_diff_bump.convolution_tendsto_right_of_continuous {G : Type uG} {E' : Type uE'} {g : G E'} {μ : measure_theory.measure G} [ E'] [ G] [complete_space E'] [borel_space G] {ι : Type u_1} {φ : ι } {l : filter ι} (hφ : filter.tendsto (λ (i : ι), (φ i).R) l (nhds 0)) (hg : continuous g) (x₀ : G) :
filter.tendsto (λ (i : ι), convolution (λ (x : G), (φ i).normed μ x) g μ x₀) l (nhds (g x₀))

Special case of `cont_diff_bump.convolution_tendsto_right` where `g` is continuous, and the limit is taken only in the first function.

theorem integral_convolution {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} {g : G E'} [is_R_or_C 𝕜] [ E] [ E'] [ F] [ F] {μ ν : measure_theory.measure G} (L : E →L[𝕜] E' →L[𝕜] F) [add_group G] [ E] [ E'] [complete_space E'] (hf : ν) (hg : μ) :
(x : G), g L ν x μ = (L ( (x : G), f x ν)) ( (x : G), g x μ)
theorem convolution_assoc' {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {E'' : Type uE''} {F : Type uF} {F' : Type uF'} {F'' : Type uF''} {f : G E} {g : G E'} [is_R_or_C 𝕜] [ E] [ E'] [ E''] [ F] [ F] {μ ν : measure_theory.measure G} (L : E →L[𝕜] E' →L[𝕜] F) [ F'] [ F'] [complete_space F'] [ F''] [ F''] [complete_space F''] {k : G E''} (L₂ : F →L[𝕜] E'' →L[𝕜] F') (L₃ : E →L[𝕜] F'' →L[𝕜] F') (L₄ : E' →L[𝕜] E'' →L[𝕜] F'') [add_group G] (hL : (x : E) (y : E') (z : E''), (L₂ ((L x) y)) z = (L₃ x) ((L₄ y) z)) {x₀ : G} (hfg : ∀ᵐ (y : G) μ, L ν) (hgk : ∀ᵐ (x : G) ν, L₄ μ) (hi : measure_theory.integrable (function.uncurry (λ (x y : G), (L₃ (f y)) ((L₄ (g (x - y))) (k (x₀ - x))))) (μ.prod ν)) :
convolution g L ν) k L₂ μ x₀ = k L₄ μ) L₃ ν x₀

Convolution is associative. This has a weak but inconvenient integrability condition. See also `convolution_assoc`.

theorem convolution_assoc {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {E'' : Type uE''} {F : Type uF} {F' : Type uF'} {F'' : Type uF''} {f : G E} {g : G E'} [is_R_or_C 𝕜] [ E] [ E'] [ E''] [ F] [ F] {μ ν : measure_theory.measure G} (L : E →L[𝕜] E' →L[𝕜] F) [ F'] [ F'] [complete_space F'] [ F''] [ F''] [complete_space F''] {k : G E''} (L₂ : F →L[𝕜] E'' →L[𝕜] F') (L₃ : E →L[𝕜] F'' →L[𝕜] F') (L₄ : E' →L[𝕜] E'' →L[𝕜] F'') [add_group G] (hL : (x : E) (y : E') (z : E''), (L₂ ((L x) y)) z = (L₃ x) ((L₄ y) z)) {x₀ : G} (hfg : ∀ᵐ (y : G) μ, L ν) (hgk : ∀ᵐ (x : G) ν, convolution_exists_at (λ (x : G), g x) (λ (x : G), k x) x μ) (hfgk : convolution_exists_at (λ (x : G), f x) (convolution (λ (x : G), g x) (λ (x : G), k x) μ) x₀ ν) :
convolution g L ν) k L₂ μ x₀ = k L₄ μ) L₃ ν x₀

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 at `x₀`
theorem convolution_precompR_apply {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {E'' : Type uE''} {F : Type uF} {f : G E} [is_R_or_C 𝕜] [ E] [ E'] [ E''] [ F] [ F] {μ : measure_theory.measure G} (L : E →L[𝕜] E' →L[𝕜] F) [borel_space G] {g : G (E'' →L[𝕜] E')} (hf : μ) (hcg : has_compact_support g) (hg : continuous g) (x₀ : G) (x : E'') :
g μ x₀) x = (λ (a : G), (g a) x) L μ x₀
theorem has_compact_support.has_fderiv_at_convolution_right {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} {g : G E'} [is_R_or_C 𝕜] [ E] [ E'] [ F] [ F] {μ : measure_theory.measure G} (L : E →L[𝕜] E' →L[𝕜] F) [borel_space G] [ G] (hcg : has_compact_support g) (hf : μ) (hg : 1 g) (x₀ : G) :
has_fderiv_at g L μ) (fderiv 𝕜 g) μ x₀) x₀

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 `continuous_linear_map.precompR`.

theorem has_compact_support.has_fderiv_at_convolution_left {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} {g : G E'} [is_R_or_C 𝕜] [ E] [ E'] [ F] [ F] {μ : measure_theory.measure G} (L : E →L[𝕜] E' →L[𝕜] F) [borel_space G] [ G] [μ.is_neg_invariant] (hcf : has_compact_support f) (hf : 1 f) (hg : μ) (x₀ : G) :
has_fderiv_at g L μ) (convolution (fderiv 𝕜 f) g μ x₀) x₀

The one-variable case

theorem has_compact_support.has_deriv_at_convolution_right {𝕜 : Type u𝕜} {E : Type uE} {E' : Type uE'} {F : Type uF} [is_R_or_C 𝕜] [ E] [ E'] [ F] [ F] {f₀ : 𝕜 E} {g₀ : 𝕜 E'} (L : E →L[𝕜] E' →L[𝕜] F) {μ : measure_theory.measure 𝕜} (hf : μ) (hcg : has_compact_support g₀) (hg : 1 g₀) (x₀ : 𝕜) :
has_deriv_at (convolution f₀ g₀ L μ) (convolution f₀ (deriv g₀) L μ x₀) x₀
theorem has_compact_support.has_deriv_at_convolution_left {𝕜 : Type u𝕜} {E : Type uE} {E' : Type uE'} {F : Type uF} [is_R_or_C 𝕜] [ E] [ E'] [ F] [ F] {f₀ : 𝕜 E} {g₀ : 𝕜 E'} (L : E →L[𝕜] E' →L[𝕜] F) {μ : measure_theory.measure 𝕜} [μ.is_neg_invariant] (hcf : has_compact_support f₀) (hf : 1 f₀) (hg : μ) (x₀ : 𝕜) :
has_deriv_at (convolution f₀ g₀ L μ) (convolution (deriv f₀) g₀ L μ x₀) x₀
theorem has_fderiv_at_convolution_right_with_param {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {P : Type uP} {f : G E} [is_R_or_C 𝕜] [ E] [ E'] [ F] [ F] [borel_space G] [ G] [ P] {μ : measure_theory.measure G} (L : E →L[𝕜] E' →L[𝕜] F) {g : P G E'} {s : set P} {k : set G} (hs : is_open s) (hk : is_compact k) (hgs : (p : P) (x : G), p s x k g p x = 0) (hf : μ) (hg : 1 g (s ×ˢ set.univ)) (q₀ : P × G) (hq₀ : q₀.fst s) :
has_fderiv_at (λ (q : P × G), (g q.fst) L μ q.snd) (λ (x : G), g (q₀.fst, x)) L) μ q₀.snd) q₀

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`).

theorem cont_diff_on_convolution_right_with_param_aux {𝕜 : Type u𝕜} {E : Type uE} [is_R_or_C 𝕜] [ E] {G E' F P : Type uP} [ E'] [ F] [ F] {μ : measure_theory.measure G} [borel_space G] [ G] [ P] {f : G E} {n : ℕ∞} (L : E →L[𝕜] E' →L[𝕜] F) {g : P G E'} {s : set P} {k : set G} (hs : is_open s) (hk : is_compact k) (hgs : (p : P) (x : G), p s x k g p x = 0) (hf : μ) (hg : n g (s ×ˢ set.univ)) :
n (λ (q : P × G), (g q.fst) L μ q.snd) (s ×ˢ set.univ)

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 `cont_diff_on_convolution_right_with_param`, which removes this restriction.

theorem cont_diff_on_convolution_right_with_param {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {P : Type uP} [is_R_or_C 𝕜] [ E] [ E'] [ F] [ F] [borel_space G] [ G] [ P] {μ : measure_theory.measure G} {f : G E} {n : ℕ∞} (L : E →L[𝕜] E' →L[𝕜] F) {g : P G E'} {s : set P} {k : set G} (hs : is_open s) (hk : is_compact k) (hgs : (p : P) (x : G), p s x k g p x = 0) (hf : μ) (hg : n g (s ×ˢ set.univ)) :
n (λ (q : P × G), (g q.fst) L μ q.snd) (s ×ˢ set.univ)

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`).

theorem cont_diff_on_convolution_right_with_param_comp {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {P : Type uP} [is_R_or_C 𝕜] [ E] [ E'] [ F] [ F] [borel_space G] [ G] [ P] {μ : measure_theory.measure G} {n : ℕ∞} (L : E →L[𝕜] E' →L[𝕜] F) {s : set P} {v : P G} (hv : n v s) {f : G E} {g : P G E'} {k : set G} (hs : is_open s) (hk : is_compact k) (hgs : (p : P) (x : G), p s x k g p x = 0) (hf : μ) (hg : n g (s ×ˢ set.univ)) :
n (λ (x : P), (g x) L μ (v x)) 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.

theorem cont_diff_on_convolution_left_with_param {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {P : Type uP} [is_R_or_C 𝕜] [ E] [ E'] [ F] [ F] [borel_space G] [ G] [ P] {μ : measure_theory.measure G} [μ.is_neg_invariant] (L : E' →L[𝕜] E →L[𝕜] F) {f : G E} {n : ℕ∞} {g : P G E'} {s : set P} {k : set G} (hs : is_open s) (hk : is_compact k) (hgs : (p : P) (x : G), p s x k g p x = 0) (hf : μ) (hg : n g (s ×ˢ set.univ)) :
n (λ (q : P × G), convolution (g q.fst) f L μ q.snd) (s ×ˢ set.univ)

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`).

theorem cont_diff_on_convolution_left_with_param_comp {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {P : Type uP} [is_R_or_C 𝕜] [ E] [ E'] [ F] [ F] [borel_space G] [ G] [ P] {μ : measure_theory.measure G} [μ.is_neg_invariant] (L : E' →L[𝕜] E →L[𝕜] F) {s : set P} {n : ℕ∞} {v : P G} (hv : n v s) {f : G E} {g : P G E'} {k : set G} (hs : is_open s) (hk : is_compact k) (hgs : (p : P) (x : G), p s x k g p x = 0) (hf : μ) (hg : n g (s ×ˢ set.univ)) :
n (λ (x : P), convolution (g x) f L μ (v x)) 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.

theorem has_compact_support.cont_diff_convolution_right {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} {g : G E'} [is_R_or_C 𝕜] [ E] [ E'] [ F] [ F] [borel_space G] [ G] {μ : measure_theory.measure G} (L : E →L[𝕜] E' →L[𝕜] F) {n : ℕ∞} (hcg : has_compact_support g) (hf : μ) (hg : n g) :
n g L μ)
theorem has_compact_support.cont_diff_convolution_left {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {f : G E} {g : G E'} [is_R_or_C 𝕜] [ E] [ E'] [ F] [ F] [borel_space G] [ G] {μ : measure_theory.measure G} (L : E →L[𝕜] E' →L[𝕜] F) [μ.is_neg_invariant] {n : ℕ∞} (hcf : has_compact_support f) (hf : n f) (hg : μ) :
n g L μ)
noncomputable def pos_convolution {E : Type uE} {E' : Type uE'} {F : Type uF} [ E] [ E'] [ F] (f : E) (g : E') (L : E →L[] E' →L[] F) (ν : . "volume_tac") :

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
theorem pos_convolution_eq_convolution_indicator {E : Type uE} {E' : Type uE'} {F : Type uF} [ E] [ E'] [ F] (f : E) (g : E') (L : E →L[] E' →L[] F) (ν : . "volume_tac")  :
L ν = convolution ((set.Ioi 0).indicator f) ((set.Ioi 0).indicator g) L ν
theorem integrable_pos_convolution {E : Type uE} {E' : Type uE'} {F : Type uF} [ E] [ E'] [ F] {f : E} {g : E'} {μ ν : measure_theory.measure } (hf : ν) (hg : μ) (L : E →L[] E' →L[] F) :
theorem integral_pos_convolution {E : Type uE} {E' : Type uE'} {F : Type uF} [ E] [ E'] [ F] [complete_space E'] {μ ν : measure_theory.measure } {f : E} {g : E'} (hf : ν) (hg : μ) (L : E →L[] E' →L[] F) :
(x : ) in , (t : ) in 0..x, (L (f t)) (g (x - t)) ν μ = (L ( (x : ) in , f x ν)) ( (x : ) in , g x μ)

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.)