mathlib documentation

analysis.convolution

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 = 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

Main Definitions #

Main Results #

Notation #

The following notations are localized in the locale convolution:

To do #

theorem has_compact_support.convolution_integrand_bound_right {𝕜 : Type u_1} {G : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [normed_add_comm_group E] [normed_add_comm_group E'] [normed_add_comm_group F] {f : G E} {g : G E'} [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 E'] [normed_space 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [add_group G] [topological_space G] (hcg : has_compact_support g) (hg : continuous g) {x t : G} {s : set G} (hx : x s) :
(L (f t)) (g (x - t)) (-tsupport g + s).indicator (λ (t : G), L * f t * (i : G), g i) t
theorem continuous.convolution_integrand_fst {𝕜 : Type u_1} {G : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [normed_add_comm_group E] [normed_add_comm_group E'] [normed_add_comm_group F] {f : G E} {g : G E'} [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 E'] [normed_space 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [add_group G] [topological_space G] [has_continuous_sub 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_1} {G : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [normed_add_comm_group E] [normed_add_comm_group E'] [normed_add_comm_group F] {f : G E} {g : G E'} [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 E'] [normed_space 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [add_group G] [topological_space G] (hcf : has_compact_support f) (hf : continuous f) {x t : G} {s : set G} (hx : x s) :
(L (f (x - t))) (g t) (-tsupport f + s).indicator (λ (t : G), (L * (i : G), f i) * g t) t
def convolution_exists_at {𝕜 : Type u_1} {G : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [normed_add_comm_group E] [normed_add_comm_group E'] [normed_add_comm_group F] [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 E'] [normed_space 𝕜 F] [measurable_space G] [has_sub G] (f : G E) (g : G E') (x : G) (L : E →L[𝕜] E' →L[𝕜] F) (μ : measure_theory.measure G . "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_1} {G : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [normed_add_comm_group E] [normed_add_comm_group E'] [normed_add_comm_group F] [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 E'] [normed_space 𝕜 F] [measurable_space G] [has_sub G] (f : G E) (g : G E') (L : E →L[𝕜] E' →L[𝕜] F) (μ : measure_theory.measure G . "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
theorem convolution_exists_at.integrable {𝕜 : Type u_1} {G : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [normed_add_comm_group E] [normed_add_comm_group E'] [normed_add_comm_group F] {f : G E} {g : G E'} [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 E'] [normed_space 𝕜 F] {L : E →L[𝕜] E' →L[𝕜] F} [measurable_space G] {μ : measure_theory.measure G} [has_sub G] {x : G} (h : convolution_exists_at f g x L μ) :
measure_theory.integrable (λ (t : G), (L (f t)) (g (x - t))) μ
theorem bdd_above.convolution_exists_at' {𝕜 : Type u_1} {G : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [normed_add_comm_group E] [normed_add_comm_group E'] [normed_add_comm_group F] {f : G E} {g : G E'} [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 E'] [normed_space 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [measurable_space G] {μ : measure_theory.measure G} [add_group G] [has_measurable_add₂ G] [has_measurable_neg 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 : measure_theory.integrable_on f s μ) (hmf : measure_theory.ae_strongly_measurable f μ) (hmg : measure_theory.ae_strongly_measurable g (measure_theory.measure.map (λ (t : G), x₀ - t) μ)) :
convolution_exists_at f g 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.

Note: we could weaken the measurability condition to hold only for μ.restrict s.

theorem convolution_exists_at.of_norm' {𝕜 : Type u_1} {G : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [normed_add_comm_group E] [normed_add_comm_group E'] [normed_add_comm_group F] {f : G E} {g : G E'} [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 E'] [normed_space 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [measurable_space G] {μ : measure_theory.measure G} [add_group G] [has_measurable_add₂ G] [has_measurable_neg G] {x₀ : G} (h : convolution_exists_at (λ (x : G), f x) (λ (x : G), g x) x₀ (continuous_linear_map.mul ) μ) (hmf : measure_theory.ae_strongly_measurable f μ) (hmg : measure_theory.ae_strongly_measurable g (measure_theory.measure.map (λ (t : G), x₀ - t) μ)) :
convolution_exists_at f g x₀ L μ

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

theorem convolution_exists_at.of_norm {𝕜 : Type u_1} {G : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [normed_add_comm_group E] [normed_add_comm_group E'] [normed_add_comm_group F] {f : G E} {g : G E'} [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 E'] [normed_space 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [measurable_space G] {μ : measure_theory.measure G} [add_group G] [has_measurable_add₂ G] [has_measurable_neg G] [measure_theory.sigma_finite μ] [μ.is_add_right_invariant] {x₀ : G} (h : convolution_exists_at (λ (x : G), f x) (λ (x : G), g x) x₀ (continuous_linear_map.mul ) μ) (hmf : measure_theory.ae_strongly_measurable f μ) (hmg : measure_theory.ae_strongly_measurable g μ) :
convolution_exists_at f g x₀ L μ

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

theorem bdd_above.convolution_exists_at {𝕜 : Type u_1} {G : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [normed_add_comm_group E] [normed_add_comm_group E'] [normed_add_comm_group F] {f : G E} {g : G E'} [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 E'] [normed_space 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [measurable_space G] {μ : measure_theory.measure G} [add_comm_group G] [has_measurable_add₂ G] [has_measurable_neg G] [μ.is_add_left_invariant] [measure_theory.sigma_finite μ] {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 : measure_theory.integrable_on f s μ) (hmf : measure_theory.ae_strongly_measurable f μ) (hmg : measure_theory.ae_strongly_measurable g μ) :
convolution_exists_at f g 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_1} {G : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [normed_add_comm_group E] [normed_add_comm_group E'] [normed_add_comm_group F] {f : G E} {g : G E'} {x : G} [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 E'] [normed_space 𝕜 F] {L : E →L[𝕜] E' →L[𝕜] F} [measurable_space G] {μ : measure_theory.measure G} [add_comm_group G] [has_measurable_add₂ G] [has_measurable_neg G] [μ.is_add_left_invariant] [μ.is_neg_invariant] :
theorem convolution_exists_at.integrable_swap {𝕜 : Type u_1} {G : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [normed_add_comm_group E] [normed_add_comm_group E'] [normed_add_comm_group F] {f : G E} {g : G E'} {x : G} [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 E'] [normed_space 𝕜 F] {L : E →L[𝕜] E' →L[𝕜] F} [measurable_space G] {μ : measure_theory.measure G} [add_comm_group G] [has_measurable_add₂ G] [has_measurable_neg G] [μ.is_add_left_invariant] [μ.is_neg_invariant] (h : convolution_exists_at f g x L μ) :
measure_theory.integrable (λ (t : G), (L (f (x - t))) (g t)) μ
theorem convolution_exists_at_iff_integrable_swap {𝕜 : Type u_1} {G : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [normed_add_comm_group E] [normed_add_comm_group E'] [normed_add_comm_group F] {f : G E} {g : G E'} {x : G} [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 E'] [normed_space 𝕜 F] {L : E →L[𝕜] E' →L[𝕜] F} [measurable_space G] {μ : measure_theory.measure G} [add_comm_group G] [has_measurable_add₂ G] [has_measurable_neg G] [μ.is_add_left_invariant] [μ.is_neg_invariant] :
convolution_exists_at f g x L μ measure_theory.integrable (λ (t : G), (L (f (x - t))) (g t)) μ
noncomputable def convolution {𝕜 : Type u_1} {G : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [normed_add_comm_group E] [normed_add_comm_group E'] [normed_add_comm_group F] [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 E'] [normed_space 𝕜 F] [measurable_space G] [normed_space F] [complete_space F] [has_sub G] (f : G E) (g : G E') (L : E →L[𝕜] E' →L[𝕜] F) (μ : measure_theory.measure G . "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_1} {G : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [normed_add_comm_group E] [normed_add_comm_group E'] [normed_add_comm_group F] {f : G E} {g : G E'} {x : G} [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 E'] [normed_space 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [measurable_space G] {μ : measure_theory.measure G} [normed_space F] [complete_space F] [has_sub G] :
convolution f g L μ x = (t : G), (L (f t)) (g (x - t)) μ
theorem convolution_lsmul {𝕜 : Type u_1} {G : Type u_2} {F : Type u_6} [normed_add_comm_group F] {x : G} [nontrivially_normed_field 𝕜] [normed_space 𝕜 F] [measurable_space G] {μ : measure_theory.measure G} [normed_space F] [complete_space F] [has_sub G] {f : G 𝕜} {g : G F} :
convolution f g (continuous_linear_map.lsmul 𝕜 𝕜) μ 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_1} {G : Type u_2} {x : G} [nontrivially_normed_field 𝕜] [measurable_space G] {μ : measure_theory.measure G} [has_sub G] [normed_space 𝕜] [complete_space 𝕜] {f g : G 𝕜} :
convolution f g (continuous_linear_map.mul 𝕜 𝕜) μ x = (t : G), f t * g (x - t) μ

The definition of convolution where the bilinear operator is multiplication.

theorem smul_convolution {𝕜 : Type u_1} {G : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [normed_add_comm_group E] [normed_add_comm_group E'] [normed_add_comm_group F] {f : G E} {g : G E'} [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 E'] [normed_space 𝕜 F] {L : E →L[𝕜] E' →L[𝕜] F} [measurable_space G] {μ : measure_theory.measure G} [normed_space F] [complete_space F] [add_group G] [smul_comm_class 𝕜 F] {y : 𝕜} :
convolution (y f) g L μ = y convolution f g L μ
theorem convolution_smul {𝕜 : Type u_1} {G : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [normed_add_comm_group E] [normed_add_comm_group E'] [normed_add_comm_group F] {f : G E} {g : G E'} [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 E'] [normed_space 𝕜 F] {L : E →L[𝕜] E' →L[𝕜] F} [measurable_space G] {μ : measure_theory.measure G} [normed_space F] [complete_space F] [add_group G] [smul_comm_class 𝕜 F] {y : 𝕜} :
convolution f (y g) L μ = y convolution f g L μ
@[simp]
theorem zero_convolution {𝕜 : Type u_1} {G : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [normed_add_comm_group E] [normed_add_comm_group E'] [normed_add_comm_group F] {g : G E'} [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 E'] [normed_space 𝕜 F] {L : E →L[𝕜] E' →L[𝕜] F} [measurable_space G] {μ : measure_theory.measure G} [normed_space F] [complete_space F] [add_group G] :
convolution 0 g L μ = 0
@[simp]
theorem convolution_zero {𝕜 : Type u_1} {G : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [normed_add_comm_group E] [normed_add_comm_group E'] [normed_add_comm_group F] {f : G E} [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 E'] [normed_space 𝕜 F] {L : E →L[𝕜] E' →L[𝕜] F} [measurable_space G] {μ : measure_theory.measure G} [normed_space F] [complete_space F] [add_group G] :
convolution f 0 L μ = 0
theorem convolution_exists_at.distrib_add {𝕜 : Type u_1} {G : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [normed_add_comm_group E] [normed_add_comm_group E'] [normed_add_comm_group F] {f : G E} {g g' : G E'} [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 E'] [normed_space 𝕜 F] {L : E →L[𝕜] E' →L[𝕜] F} [measurable_space G] {μ : measure_theory.measure G} [normed_space F] [complete_space F] [add_group G] {x : G} (hfg : convolution_exists_at f g x L μ) (hfg' : convolution_exists_at f g' x L μ) :
convolution f (g + g') L μ x = convolution f g L μ x + convolution f g' L μ x
theorem convolution_exists.distrib_add {𝕜 : Type u_1} {G : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [normed_add_comm_group E] [normed_add_comm_group E'] [normed_add_comm_group F] {f : G E} {g g' : G E'} [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 E'] [normed_space 𝕜 F] {L : E →L[𝕜] E' →L[𝕜] F} [measurable_space G] {μ : measure_theory.measure G} [normed_space F] [complete_space F] [add_group G] (hfg : convolution_exists f g L μ) (hfg' : convolution_exists f g' L μ) :
convolution f (g + g') L μ = convolution f g L μ + convolution f g' L μ
theorem convolution_exists_at.add_distrib {𝕜 : Type u_1} {G : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [normed_add_comm_group E] [normed_add_comm_group E'] [normed_add_comm_group F] {f f' : G E} {g : G E'} [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 E'] [normed_space 𝕜 F] {L : E →L[𝕜] E' →L[𝕜] F} [measurable_space G] {μ : measure_theory.measure G} [normed_space F] [complete_space F] [add_group G] {x : G} (hfg : convolution_exists_at f g x L μ) (hfg' : convolution_exists_at f' g x L μ) :
convolution (f + f') g L μ x = convolution f g L μ x + convolution f' g L μ x
theorem convolution_exists.add_distrib {𝕜 : Type u_1} {G : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [normed_add_comm_group E] [normed_add_comm_group E'] [normed_add_comm_group F] {f f' : G E} {g : G E'} [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 E'] [normed_space 𝕜 F] {L : E →L[𝕜] E' →L[𝕜] F} [measurable_space G] {μ : measure_theory.measure G} [normed_space F] [complete_space F] [add_group G] (hfg : convolution_exists f g L μ) (hfg' : convolution_exists f' g L μ) :
convolution (f + f') g L μ = convolution f g L μ + convolution f' g L μ
theorem convolution_congr {𝕜 : Type u_1} {G : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [normed_add_comm_group E] [normed_add_comm_group E'] [normed_add_comm_group F] {f f' : G E} {g g' : G E'} [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 E'] [normed_space 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [measurable_space G] {μ : measure_theory.measure G} [normed_space F] [complete_space F] [add_group G] [has_measurable_add₂ G] [has_measurable_neg G] [measure_theory.sigma_finite μ] [μ.is_add_right_invariant] (h1 : f =ᵐ[μ] f') (h2 : g =ᵐ[μ] g') :
convolution f g L μ = convolution f' g' L μ
theorem support_convolution_subset_swap {𝕜 : Type u_1} {G : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [normed_add_comm_group E] [normed_add_comm_group E'] [normed_add_comm_group F] {f : G E} {g : G E'} [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 E'] [normed_space 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [measurable_space G] {μ : measure_theory.measure G} [normed_space F] [complete_space F] [add_group G] :

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.

A version of has_compact_support.continuous_convolution_right that works if G is not locally compact but requires that g is integrable.

theorem support_convolution_subset {𝕜 : Type u_1} {G : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [normed_add_comm_group E] [normed_add_comm_group E'] [normed_add_comm_group F] {f : G E} {g : G E'} [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 E'] [normed_space 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [measurable_space G] {μ : measure_theory.measure G} [normed_space F] [complete_space F] [add_comm_group G] :
theorem convolution_flip {𝕜 : Type u_1} {G : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [normed_add_comm_group E] [normed_add_comm_group E'] [normed_add_comm_group F] {f : G E} {g : G E'} [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 E'] [normed_space 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [measurable_space G] {μ : measure_theory.measure G} [normed_space F] [complete_space F] [add_comm_group G] [μ.is_add_left_invariant] [μ.is_neg_invariant] [has_measurable_neg G] [has_measurable_add G] :
convolution g f L.flip μ = convolution f g L μ

Commutativity of convolution

theorem convolution_eq_swap {𝕜 : Type u_1} {G : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [normed_add_comm_group E] [normed_add_comm_group E'] [normed_add_comm_group F] {f : G E} {g : G E'} {x : G} [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 E'] [normed_space 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [measurable_space G] {μ : measure_theory.measure G} [normed_space F] [complete_space F] [add_comm_group G] [μ.is_add_left_invariant] [μ.is_neg_invariant] [has_measurable_neg G] [has_measurable_add G] :
convolution f g L μ x = (t : G), (L (f (x - t))) (g t) μ

The symmetric definition of convolution.

theorem convolution_lsmul_swap {𝕜 : Type u_1} {G : Type u_2} {F : Type u_6} [normed_add_comm_group F] {x : G} [nontrivially_normed_field 𝕜] [normed_space 𝕜 F] [measurable_space G] {μ : measure_theory.measure G} [normed_space F] [complete_space F] [add_comm_group G] [μ.is_add_left_invariant] [μ.is_neg_invariant] [has_measurable_neg G] [has_measurable_add G] {f : G 𝕜} {g : G F} :
convolution f g (continuous_linear_map.lsmul 𝕜 𝕜) μ 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_1} {G : Type u_2} {x : G} [nontrivially_normed_field 𝕜] [measurable_space G] {μ : measure_theory.measure G} [add_comm_group G] [μ.is_add_left_invariant] [μ.is_neg_invariant] [has_measurable_neg G] [has_measurable_add G] [normed_space 𝕜] [complete_space 𝕜] {f g : G 𝕜} :
convolution f g (continuous_linear_map.mul 𝕜 𝕜) μ 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_1} {G : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [normed_add_comm_group E] [normed_add_comm_group E'] [normed_add_comm_group F] {f : G E} {g : G E'} {x : G} [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 E'] [normed_space 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [measurable_space G] {μ : measure_theory.measure G} [normed_space F] [complete_space F] [add_comm_group G] [μ.is_add_left_invariant] [μ.is_neg_invariant] [has_measurable_neg G] [has_measurable_add G] (h1 : ∀ᵐ (x : G) μ, f (-x) = f x) (h2 : ∀ᵐ (x : G) μ, g (-x) = g x) :
convolution f g L μ (-x) = convolution f g L μ x

The convolution of two even functions is also even.

theorem convolution_eq_right' {𝕜 : Type u_1} {G : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [normed_add_comm_group E] [normed_add_comm_group E'] [normed_add_comm_group F] {f : G E} {g : G E'} [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 E'] [normed_space 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [measurable_space G] {μ : measure_theory.measure G} [normed_space F] [complete_space F] [seminormed_add_comm_group G] {x₀ : G} {R : } (hf : function.support f metric.ball 0 R) (hg : (x : G), x metric.ball x₀ R g x = g x₀) :
convolution f 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_1} {G : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [normed_add_comm_group E] [normed_add_comm_group E'] [normed_add_comm_group F] {f : G E} {g : G E'} [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 E'] [normed_space 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [measurable_space G] {μ : measure_theory.measure G} [normed_space F] [complete_space F] [seminormed_add_comm_group G] [borel_space G] [topological_space.second_countable_topology G] [μ.is_add_left_invariant] [measure_theory.sigma_finite μ] {x₀ : G} {R ε : } {z₀ : E'} (hε : 0 ε) (hif : measure_theory.integrable f μ) (hf : function.support f metric.ball 0 R) (hmg : measure_theory.ae_strongly_measurable g μ) (hg : (x : G), x metric.ball x₀ R has_dist.dist (g x) z₀ ε) :
has_dist.dist (convolution f 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 u_2} {E' : Type u_4} [normed_add_comm_group E'] {g : G E'} [measurable_space G] {μ : measure_theory.measure G} [seminormed_add_comm_group G] [borel_space G] [topological_space.second_countable_topology G] [μ.is_add_left_invariant] [measure_theory.sigma_finite μ] [normed_space E'] [complete_space E'] {f : G } {x₀ : G} {R ε : } {z₀ : E'} (hε : 0 ε) (hf : function.support f metric.ball 0 R) (hnf : (x : G), 0 f x) (hintf : (x : G), f x μ = 1) (hmg : measure_theory.ae_strongly_measurable g μ) (hg : (x : G), x metric.ball x₀ R has_dist.dist (g 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 u_2} {E' : Type u_4} [normed_add_comm_group E'] [measurable_space G] {μ : measure_theory.measure G} [seminormed_add_comm_group G] [borel_space G] [topological_space.second_countable_topology G] [μ.is_add_left_invariant] [measure_theory.sigma_finite μ] [normed_space 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, measure_theory.ae_strongly_measurable (g i) μ) (hcg : filter.tendsto (function.uncurry g) (l.prod (nhds x₀)) (nhds z₀)) (hk : filter.tendsto k l (nhds x₀)) :
filter.tendsto (λ (i : ι), convolution (φ i) (g i) (continuous_linear_map.lsmul ) μ (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_of_inner.convolution_tendsto_right.

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

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

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_of_inner.convolution_tendsto_right {G : Type u_2} {E' : Type u_4} [normed_add_comm_group E'] [measurable_space G] {μ : measure_theory.measure G} [normed_space E'] [inner_product_space G] [complete_space E'] [borel_space G] [measure_theory.is_locally_finite_measure μ] [μ.is_open_pos_measure] [finite_dimensional G] [μ.is_add_left_invariant] {ι : Type u_1} {φ : ι cont_diff_bump_of_inner 0} {g : ι G E'} {k : ι G} {x₀ : G} {z₀ : E'} {l : filter ι} (hφ : filter.tendsto (λ (i : ι), (φ i).R) l (nhds 0)) (hig : ∀ᶠ (i : ι) in l, measure_theory.ae_strongly_measurable (g i) μ) (hcg : filter.tendsto (function.uncurry g) (l.prod (nhds x₀)) (nhds z₀)) (hk : filter.tendsto k l (nhds x₀)) :
filter.tendsto (λ (i : ι), convolution (λ (x : G), (φ i).normed μ x) (g i) (continuous_linear_map.lsmul ) μ (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_of_inner.convolution_tendsto_right_of_continuous {G : Type u_2} {E' : Type u_4} [normed_add_comm_group E'] {g : G E'} [measurable_space G] {μ : measure_theory.measure G} [normed_space E'] [inner_product_space G] [complete_space E'] [borel_space G] [measure_theory.is_locally_finite_measure μ] [μ.is_open_pos_measure] [finite_dimensional G] [μ.is_add_left_invariant] {ι : Type u_1} {φ : ι cont_diff_bump_of_inner 0} {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 (continuous_linear_map.lsmul ) μ x₀) l (nhds (g x₀))

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

theorem integral_convolution {𝕜 : Type u_1} {G : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [normed_add_comm_group E] [normed_add_comm_group E'] [normed_add_comm_group F] {f : G E} {g : G E'} [is_R_or_C 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 E'] [normed_space F] [normed_space 𝕜 F] [complete_space F] [measurable_space G] {μ ν : measure_theory.measure G} (L : E →L[𝕜] E' →L[𝕜] F) [add_group G] [measure_theory.sigma_finite μ] [measure_theory.sigma_finite ν] [μ.is_add_right_invariant] [has_measurable_add₂ G] [has_measurable_neg G] [normed_space E] [normed_space E'] [complete_space E] [complete_space E'] (hf : measure_theory.integrable f ν) (hg : measure_theory.integrable g μ) :
(x : G), convolution f g L ν x μ = (L ( (x : G), f x ν)) ( (x : G), g x μ)
theorem convolution_assoc' {𝕜 : Type u_1} {G : Type u_2} {E : Type u_3} {E' : Type u_4} {E'' : Type u_5} {F : Type u_6} {F' : Type u_7} {F'' : Type u_8} [normed_add_comm_group E] [normed_add_comm_group E'] [normed_add_comm_group E''] [normed_add_comm_group F] {f : G E} {g : G E'} [is_R_or_C 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 E'] [normed_space 𝕜 E''] [normed_space F] [normed_space 𝕜 F] [complete_space F] [measurable_space G] {μ ν : measure_theory.measure G} (L : E →L[𝕜] E' →L[𝕜] F) [normed_add_comm_group F'] [normed_space F'] [normed_space 𝕜 F'] [complete_space F'] [normed_add_comm_group F''] [normed_space F''] [normed_space 𝕜 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] [measure_theory.sigma_finite μ] [measure_theory.sigma_finite ν] [μ.is_add_right_invariant] [has_measurable_add₂ G] [ν.is_add_right_invariant] [has_measurable_neg G] (hL : (x : E) (y : E') (z : E''), (L₂ ((L x) y)) z = (L₃ x) ((L₄ y) z)) {x₀ : G} (hfg : ∀ᵐ (y : G) μ, convolution_exists_at f g y L ν) (hgk : ∀ᵐ (x : G) ν, convolution_exists_at g k x L₄ μ) (hi : measure_theory.integrable (function.uncurry (λ (x y : G), (L₃ (f y)) ((L₄ (g (x - y))) (k (x₀ - x))))) (μ.prod ν)) :
convolution (convolution f g L ν) k L₂ μ x₀ = convolution f (convolution g k L₄ μ) L₃ ν x₀

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

theorem convolution_assoc {𝕜 : Type u_1} {G : Type u_2} {E : Type u_3} {E' : Type u_4} {E'' : Type u_5} {F : Type u_6} {F' : Type u_7} {F'' : Type u_8} [normed_add_comm_group E] [normed_add_comm_group E'] [normed_add_comm_group E''] [normed_add_comm_group F] {f : G E} {g : G E'} [is_R_or_C 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 E'] [normed_space 𝕜 E''] [normed_space F] [normed_space 𝕜 F] [complete_space F] [measurable_space G] {μ ν : measure_theory.measure G} (L : E →L[𝕜] E' →L[𝕜] F) [normed_add_comm_group F'] [normed_space F'] [normed_space 𝕜 F'] [complete_space F'] [normed_add_comm_group F''] [normed_space F''] [normed_space 𝕜 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] [measure_theory.sigma_finite μ] [measure_theory.sigma_finite ν] [μ.is_add_right_invariant] [has_measurable_add₂ G] [ν.is_add_right_invariant] [has_measurable_neg G] (hL : (x : E) (y : E') (z : E''), (L₂ ((L x) y)) z = (L₃ x) ((L₄ y) z)) {x₀ : G} (hf : measure_theory.ae_strongly_measurable f ν) (hg : measure_theory.ae_strongly_measurable g μ) (hk : measure_theory.ae_strongly_measurable k μ) (hfg : ∀ᵐ (y : G) μ, convolution_exists_at f g y L ν) (hgk : ∀ᵐ (x : G) ν, convolution_exists_at (λ (x : G), g x) (λ (x : G), k x) x (continuous_linear_map.mul ) μ) (hfgk : convolution_exists_at (λ (x : G), f x) (convolution (λ (x : G), g x) (λ (x : G), k x) (continuous_linear_map.mul ) μ) x₀ (continuous_linear_map.mul ) ν) :
convolution (convolution f g L ν) k L₂ μ x₀ = convolution f (convolution g 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_1} {G : Type u_2} {E : Type u_3} {E' : Type u_4} {E'' : Type u_5} {F : Type u_6} [normed_add_comm_group E] [normed_add_comm_group E'] [normed_add_comm_group E''] [normed_add_comm_group F] {f : G E} [is_R_or_C 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 E'] [normed_space 𝕜 E''] [normed_space F] [normed_space 𝕜 F] [complete_space F] [measurable_space G] {μ : measure_theory.measure G} (L : E →L[𝕜] E' →L[𝕜] F) [normed_add_comm_group G] [borel_space G] [normed_space 𝕜 G] {g : G (E'' →L[𝕜] E')} (hf : measure_theory.locally_integrable f μ) (hcg : has_compact_support g) (hg : continuous g) (x₀ : G) (x : E'') :
(convolution f g (continuous_linear_map.precompR E'' L) μ x₀) x = convolution f (λ (a : G), (g a) x) L μ x₀
theorem has_compact_support.has_fderiv_at_convolution_right {𝕜 : Type u_1} {G : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [normed_add_comm_group E] [normed_add_comm_group E'] [normed_add_comm_group F] {f : G E} {g : G E'} [is_R_or_C 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 E'] [normed_space F] [normed_space 𝕜 F] [complete_space F] [measurable_space G] {μ : measure_theory.measure G} (L : E →L[𝕜] E' →L[𝕜] F) [normed_add_comm_group G] [borel_space G] [normed_space 𝕜 G] [measure_theory.sigma_finite μ] [μ.is_add_left_invariant] (hcg : has_compact_support g) (hf : measure_theory.locally_integrable f μ) (hg : cont_diff 𝕜 1 g) (x₀ : G) :

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.cont_diff_convolution_right {𝕜 : Type u_1} {G : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [normed_add_comm_group E] [normed_add_comm_group E'] [normed_add_comm_group F] {f : G E} {g : G E'} [is_R_or_C 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 E'] [normed_space F] [normed_space 𝕜 F] {n : ℕ∞} [complete_space F] [measurable_space G] {μ : measure_theory.measure G} (L : E →L[𝕜] E' →L[𝕜] F) [normed_add_comm_group G] [borel_space G] [normed_space 𝕜 G] [measure_theory.sigma_finite μ] [μ.is_add_left_invariant] (hcg : has_compact_support g) (hf : measure_theory.locally_integrable f μ) (hg : cont_diff 𝕜 n g) :
cont_diff 𝕜 n (convolution f g L μ)

The one-variable case

theorem has_compact_support.has_deriv_at_convolution_right {𝕜 : Type u_1} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [normed_add_comm_group E] [normed_add_comm_group E'] [normed_add_comm_group F] [is_R_or_C 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 E'] [normed_space F] [normed_space 𝕜 F] {f₀ : 𝕜 E} {g₀ : 𝕜 E'} (L : E →L[𝕜] E' →L[𝕜] F) [complete_space F] {μ : measure_theory.measure 𝕜} [μ.is_add_left_invariant] [measure_theory.sigma_finite μ] (hf : measure_theory.locally_integrable f₀ μ) (hcg : has_compact_support g₀) (hg : cont_diff 𝕜 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_1} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [normed_add_comm_group E] [normed_add_comm_group E'] [normed_add_comm_group F] [is_R_or_C 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 E'] [normed_space F] [normed_space 𝕜 F] {f₀ : 𝕜 E} {g₀ : 𝕜 E'} (L : E →L[𝕜] E' →L[𝕜] F) [complete_space F] {μ : measure_theory.measure 𝕜} [μ.is_add_left_invariant] [measure_theory.sigma_finite μ] [μ.is_neg_invariant] (hcf : has_compact_support f₀) (hf : cont_diff 𝕜 1 f₀) (hg : measure_theory.locally_integrable g₀ μ) (x₀ : 𝕜) :
has_deriv_at (convolution f₀ g₀ L μ) (convolution (deriv f₀) g₀ L μ x₀) x₀