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 usemul/smulin 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
smulto 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 offandgw.r.t. the continuous bilinear mapLand measureμ.convolution_exists_at f g x L μstates that the convolution(f ⋆[L, μ] g) xis well-defined (i.e. the integral exists).convolution_exists f g L μstates that the convolutionf ⋆[L, μ] gis well-defined at each point.
Main Results #
has_compact_support.has_fderiv_at_convolution_rightandhas_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_rightandhas_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 around0, the convolution tends to the right argument. This is specialized to bump functions incont_diff_bump.convolution_tendsto_right.
Notation #
The following notations are localized in the locale convolution:
f ⋆[L, μ] gfor 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] gf ⋆ g := f ⋆[lsmul ℝ ℝ] g
To do #
- Existence and (uniform) continuity of the convolution if
one of the maps is in
ℒ^pand the other inℒ^qwith1 / p + 1 / q = 1. This might require a generalization ofmeasure_theory.mem_ℒp.smulwheresmulis generalized to a continuous bilinear map. (see e.g. Fremlin, Measure Theory (volume 2), 255K) - The convolution is a
ae_strongly_measurablefunction (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}
[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]
{C : ℝ}
(hC : ∀ (i : G), ‖g i‖ ≤ C)
{x t : G}
{s u : set G}
(hx : x ∈ s)
(hu : -tsupport g + s ⊆ u) :
theorem
has_compact_support.convolution_integrand_bound_right_of_subset
{𝕜 : Type u𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[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 u : set G}
(hx : x ∈ s)
(hu : -tsupport g + s ⊆ u) :
theorem
has_compact_support.convolution_integrand_bound_right
{𝕜 : Type u𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[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) :
theorem
continuous.convolution_integrand_fst
{𝕜 : Type u𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[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𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[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) :
def
convolution_exists_at
{𝕜 : Type u𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[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
- convolution_exists_at f g x L μ = measure_theory.integrable (λ (t : G), ⇑(⇑L (f t)) (g (x - t))) μ
def
convolution_exists
{𝕜 : Type u𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[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
- convolution_exists f g L μ = ∀ (x : G), convolution_exists_at f g x L μ
theorem
convolution_exists_at.integrable
{𝕜 : Type u𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[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
measure_theory.ae_strongly_measurable.convolution_integrand'
{𝕜 : Type u𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[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 ν]
(hf : measure_theory.ae_strongly_measurable f ν)
(hg : measure_theory.ae_strongly_measurable g (measure_theory.measure.map (λ (p : G × 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}
[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]
(hf : measure_theory.ae_strongly_measurable f μ)
{x : G}
(hg : measure_theory.ae_strongly_measurable g (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}
[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}
(hf : measure_theory.ae_strongly_measurable f (measure_theory.measure.map (λ (t : G), x - t) μ))
(hg : measure_theory.ae_strongly_measurable g μ) :
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}
[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 μ)
(hmg : measure_theory.ae_strongly_measurable g (measure_theory.measure.map (λ (t : G), x₀ - t) (μ.restrict s))) :
convolution_exists_at f g 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}
[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
measure_theory.ae_strongly_measurable.convolution_integrand_snd
{𝕜 : Type u𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[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]
(hf : measure_theory.ae_strongly_measurable f μ)
(hg : measure_theory.ae_strongly_measurable 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}
[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]
(hf : measure_theory.ae_strongly_measurable f μ)
(hg : measure_theory.ae_strongly_measurable 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}
[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
measure_theory.ae_strongly_measurable.convolution_integrand
{𝕜 : Type u𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[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]
[measure_theory.sigma_finite ν]
(hf : measure_theory.ae_strongly_measurable f ν)
(hg : measure_theory.ae_strongly_measurable g μ) :
theorem
measure_theory.integrable.convolution_integrand
{𝕜 : Type u𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[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]
[measure_theory.sigma_finite ν]
(hf : measure_theory.integrable f ν)
(hg : measure_theory.integrable g μ) :
theorem
measure_theory.integrable.ae_convolution_exists
{𝕜 : Type u𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[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]
[measure_theory.sigma_finite ν]
(hf : measure_theory.integrable f ν)
(hg : measure_theory.integrable g μ) :
∀ᵐ (x : G) ∂μ, convolution_exists_at f g x L ν
theorem
has_compact_support.convolution_exists_at
{𝕜 : Type u𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[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]
[topological_space G]
[topological_add_group G]
[borel_space G]
{x₀ : G}
(h : has_compact_support (λ (t : G), ⇑(⇑L (f t)) (g (x₀ - t))))
(hf : measure_theory.locally_integrable f μ)
(hg : continuous g) :
convolution_exists_at f g x₀ L μ
theorem
has_compact_support.convolution_exists_right
{𝕜 : Type u𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[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]
[topological_space G]
[topological_add_group G]
[borel_space G]
(hcg : has_compact_support g)
(hf : measure_theory.locally_integrable f μ)
(hg : continuous g) :
convolution_exists f 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}
[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]
[topological_space G]
[topological_add_group G]
[borel_space G]
(hcf : has_compact_support f)
(hf : measure_theory.locally_integrable f μ)
(hg : continuous g) :
convolution_exists f g L μ
theorem
bdd_above.convolution_exists_at
{𝕜 : Type u𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[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_neg G]
[μ.is_add_left_invariant]
[has_measurable_add₂ G]
[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 μ)
(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𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[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_neg G]
[μ.is_add_left_invariant]
[has_measurable_add G]
[μ.is_neg_invariant] :
convolution_exists_at g f x L.flip μ ↔ convolution_exists_at f g x L μ
theorem
convolution_exists_at.integrable_swap
{𝕜 : Type u𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[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_neg G]
[μ.is_add_left_invariant]
[has_measurable_add G]
[μ.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𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[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_neg G]
[μ.is_add_left_invariant]
[has_measurable_add G]
[μ.is_neg_invariant] :
convolution_exists_at f g x 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}
[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]
[topological_space G]
[topological_add_group G]
[borel_space G]
[μ.is_add_left_invariant]
[μ.is_neg_invariant]
(hcf : has_compact_support f)
(hf : continuous f)
(hg : measure_theory.locally_integrable g μ) :
convolution_exists f g 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}
[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]
[topological_space G]
[topological_add_group G]
[borel_space G]
[μ.is_add_left_invariant]
[μ.is_neg_invariant]
(hcg : has_compact_support g)
(hf : continuous f)
(hg : measure_theory.locally_integrable g μ) :
convolution_exists f g L μ
noncomputable
def
convolution
{𝕜 : Type u𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[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)) ∂μ.
theorem
convolution_def
{𝕜 : Type u𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[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] :
theorem
convolution_lsmul
{𝕜 : Type u𝕜}
{G : Type uG}
{F : Type uF}
[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𝕜}
{G : Type uG}
{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𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[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𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[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𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[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𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[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𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[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𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[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𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[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𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[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_mono_right
{G : Type uG}
{x : G}
[measurable_space G]
{μ : measure_theory.measure G}
[add_group G]
{f g g' : G → ℝ}
(hfg : convolution_exists_at f g x (continuous_linear_map.lsmul ℝ ℝ) μ)
(hfg' : convolution_exists_at f g' x (continuous_linear_map.lsmul ℝ ℝ) μ)
(hf : ∀ (x : G), 0 ≤ f x)
(hg : ∀ (x : G), g x ≤ g' x) :
convolution f g (continuous_linear_map.lsmul ℝ ℝ) μ x ≤ convolution f g' (continuous_linear_map.lsmul ℝ ℝ) μ x
theorem
convolution_mono_right_of_nonneg
{G : Type uG}
{x : G}
[measurable_space G]
{μ : measure_theory.measure G}
[add_group G]
{f g g' : G → ℝ}
(hfg' : convolution_exists_at f g' x (continuous_linear_map.lsmul ℝ ℝ) μ)
(hf : ∀ (x : G), 0 ≤ f x)
(hg : ∀ (x : G), g x ≤ g' x)
(hg' : ∀ (x : G), 0 ≤ g' x) :
convolution f g (continuous_linear_map.lsmul ℝ ℝ) μ x ≤ convolution f g' (continuous_linear_map.lsmul ℝ ℝ) μ x
theorem
convolution_congr
{𝕜 : Type u𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[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𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[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] :
function.support (convolution f g L μ) ⊆ function.support g + function.support f
theorem
measure_theory.integrable.integrable_convolution
{𝕜 : Type u𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[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]
[has_measurable_add₂ G]
[has_measurable_neg G]
[measure_theory.sigma_finite μ]
[μ.is_add_right_invariant]
(hf : measure_theory.integrable f μ)
(hg : measure_theory.integrable g μ) :
measure_theory.integrable (convolution f g L μ) μ
theorem
has_compact_support.convolution
{𝕜 : Type u𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[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]
[topological_space G]
[topological_add_group G]
[t2_space G]
(hcf : has_compact_support f)
(hcg : has_compact_support g) :
has_compact_support (convolution f g L μ)
theorem
continuous_on_convolution_right_with_param'
{𝕜 : Type u𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
{P : Type uP}
[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]
[topological_space G]
[topological_add_group G]
[borel_space G]
[topological_space.first_countable_topology G]
[topological_space P]
[topological_space.first_countable_topology P]
{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 : measure_theory.locally_integrable f μ)
(hg : continuous_on ↿g (s ×ˢ set.univ)) :
continuous_on (λ (q : P × G), convolution f (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}
[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]
[topological_space G]
[topological_add_group G]
[borel_space G]
[topological_space.first_countable_topology G]
[topological_space P]
[topological_space.first_countable_topology P]
[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 : measure_theory.locally_integrable f μ)
(hg : continuous_on ↿g (s ×ˢ set.univ)) :
continuous_on (λ (q : P × G), convolution f (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}
[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]
[topological_space G]
[topological_add_group G]
[borel_space G]
[topological_space.first_countable_topology G]
[topological_space P]
[topological_space.first_countable_topology P]
{s : set P}
{v : P → G}
(hv : continuous_on v 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 : measure_theory.locally_integrable f μ)
(hg : continuous_on ↿g (s ×ˢ set.univ)) :
continuous_on (λ (x : P), convolution f (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}
[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]
[topological_space G]
[topological_add_group G]
[borel_space G]
[topological_space.first_countable_topology G]
[topological_space P]
[topological_space.first_countable_topology P]
[t2_space G]
{s : set P}
{v : P → G}
(hv : continuous_on v 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 : measure_theory.locally_integrable f μ)
(hg : continuous_on ↿g (s ×ˢ set.univ)) :
continuous_on (λ (x : P), convolution f (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}
[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]
[topological_space G]
[topological_add_group G]
[borel_space G]
[topological_space.first_countable_topology G]
(hcg : has_compact_support g)
(hf : measure_theory.locally_integrable f μ)
(hg : continuous g) :
continuous (convolution f 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}
[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]
[topological_space G]
[topological_add_group G]
[borel_space G]
[topological_space.first_countable_topology G]
[topological_space.second_countable_topology G]
(hbg : bdd_above (set.range (λ (x : G), ‖g x‖)))
(hf : measure_theory.integrable f μ)
(hg : continuous g) :
continuous (convolution f 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}
[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] :
function.support (convolution f g L μ) ⊆ function.support f + function.support g
theorem
convolution_flip
{𝕜 : Type u𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[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𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[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] :
The symmetric definition of convolution.
theorem
convolution_lsmul_swap
{𝕜 : Type u𝕜}
{G : Type uG}
{F : Type uF}
[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𝕜}
{G : Type uG}
{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𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[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
has_compact_support.continuous_convolution_left
{𝕜 : Type u𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[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]
[topological_space G]
[topological_add_group G]
[borel_space G]
[topological_space.first_countable_topology G]
(hcf : has_compact_support f)
(hf : continuous f)
(hg : measure_theory.locally_integrable g μ) :
continuous (convolution f g L μ)
theorem
bdd_above.continuous_convolution_left_of_integrable
{𝕜 : Type u𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[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]
[topological_space G]
[topological_add_group G]
[borel_space G]
[topological_space.second_countable_topology G]
(hbf : bdd_above (set.range (λ (x : G), ‖f x‖)))
(hf : continuous f)
(hg : measure_theory.integrable g μ) :
continuous (convolution f g L μ)
theorem
convolution_eq_right'
{𝕜 : Type u𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[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₀) :
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}
[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₀ ≤ ε) :
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'}
[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₀ ≤ ε) :
has_dist.dist (convolution f g (continuous_linear_map.lsmul ℝ ℝ) μ 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'}
[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 integral1asitends tol;- The support of
φtends to small neighborhoods around(0 : G)asitends tol; g iismu-a.e. strongly measurable asitends tol;g i xtends toz₀as(i, x)tends tol ×ᶠ 𝓝 x₀;k itends tox₀.
See also cont_diff_bump.convolution_tendsto_right.
theorem
cont_diff_bump.convolution_eq_right
{G : Type uG}
{E' : Type uE'}
[normed_add_comm_group E']
{g : G → E'}
[measurable_space G]
{μ : measure_theory.measure G}
[normed_space ℝ E']
[normed_add_comm_group G]
[normed_space ℝ G]
[has_cont_diff_bump G]
[complete_space E']
{φ : cont_diff_bump 0}
{x₀ : G}
(hg : ∀ (x : G), x ∈ metric.ball x₀ φ.R → g x = g x₀) :
convolution ⇑φ g (continuous_linear_map.lsmul ℝ ℝ) μ x₀ = measure_theory.integral μ ⇑φ • 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'}
[normed_add_comm_group E']
{g : G → E'}
[measurable_space G]
{μ : measure_theory.measure G}
[normed_space ℝ E']
[normed_add_comm_group G]
[normed_space ℝ G]
[has_cont_diff_bump G]
[complete_space E']
{φ : cont_diff_bump 0}
[borel_space G]
[measure_theory.is_locally_finite_measure μ]
[μ.is_open_pos_measure]
[finite_dimensional ℝ G]
{x₀ : G}
(hg : ∀ (x : G), x ∈ metric.ball x₀ φ.R → g x = g x₀) :
convolution (φ.normed μ) g (continuous_linear_map.lsmul ℝ ℝ) μ 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'}
[normed_add_comm_group E']
{g : G → E'}
[measurable_space G]
{μ : measure_theory.measure G}
[normed_space ℝ E']
[normed_add_comm_group G]
[normed_space ℝ G]
[has_cont_diff_bump G]
[complete_space E']
{φ : cont_diff_bump 0}
[borel_space G]
[measure_theory.is_locally_finite_measure μ]
[μ.is_open_pos_measure]
[finite_dimensional ℝ G]
[μ.is_add_left_invariant]
{x₀ : G}
{ε : ℝ}
(hmg : measure_theory.ae_strongly_measurable g μ)
(hg : ∀ (x : G), x ∈ metric.ball x₀ φ.R → has_dist.dist (g x) (g x₀) ≤ ε) :
has_dist.dist (convolution (φ.normed μ) g (continuous_linear_map.lsmul ℝ ℝ) μ 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'}
[normed_add_comm_group E']
[measurable_space G]
{μ : measure_theory.measure G}
[normed_space ℝ E']
[normed_add_comm_group G]
[normed_space ℝ G]
[has_cont_diff_bump 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 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).Rtends to0asitends tol;g iismu-a.e. strongly measurable asitends tol;g i xtends toz₀as(i, x)tends tol ×ᶠ 𝓝 x₀;k itends tox₀.
theorem
cont_diff_bump.convolution_tendsto_right_of_continuous
{G : Type uG}
{E' : Type uE'}
[normed_add_comm_group E']
{g : G → E'}
[measurable_space G]
{μ : measure_theory.measure G}
[normed_space ℝ E']
[normed_add_comm_group G]
[normed_space ℝ G]
[has_cont_diff_bump 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 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.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}
[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 μ) :
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''}
[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𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{E'' : Type uE''}
{F : Type uF}
{F' : Type uF'}
{F'' : Type uF''}
[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, ν] gexists almost everywhere‖g‖ ⋆[μ] ‖k‖exists almost everywhere‖f‖ ⋆[ν] (‖g‖ ⋆[μ] ‖k‖)exists atx₀
theorem
convolution_precompR_apply
{𝕜 : Type u𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{E'' : Type uE''}
{F : Type uF}
[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]
{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𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[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) :
has_fderiv_at (convolution f g L μ) (convolution f (fderiv 𝕜 g) (continuous_linear_map.precompR G L) μ 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}
[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]
[μ.is_neg_invariant]
(hcf : has_compact_support f)
(hf : cont_diff 𝕜 1 f)
(hg : measure_theory.locally_integrable g μ)
(x₀ : G) :
has_fderiv_at (convolution f g L μ) (convolution (fderiv 𝕜 f) g (continuous_linear_map.precompL G L) μ 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}
[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𝕜}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[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₀
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}
[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 ℝ F]
[normed_space 𝕜 F]
[complete_space F]
[measurable_space G]
[normed_add_comm_group G]
[borel_space G]
[normed_space 𝕜 G]
[normed_add_comm_group P]
[normed_space 𝕜 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 : measure_theory.locally_integrable f μ)
(hg : cont_diff_on 𝕜 1 ↿g (s ×ˢ set.univ))
(q₀ : P × G)
(hq₀ : q₀.fst ∈ s) :
has_fderiv_at (λ (q : P × G), convolution f (g q.fst) L μ q.snd) (convolution f (λ (x : G), fderiv 𝕜 ↿g (q₀.fst, x)) (continuous_linear_map.precompR (P × G) 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}
[normed_add_comm_group E]
[is_R_or_C 𝕜]
[normed_space 𝕜 E]
{G E' F P : Type uP}
[normed_add_comm_group E']
[normed_add_comm_group F]
[normed_space 𝕜 E']
[normed_space ℝ F]
[normed_space 𝕜 F]
[complete_space F]
[measurable_space G]
{μ : measure_theory.measure G}
[normed_add_comm_group G]
[borel_space G]
[normed_space 𝕜 G]
[normed_add_comm_group P]
[normed_space 𝕜 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 : measure_theory.locally_integrable f μ)
(hg : cont_diff_on 𝕜 n ↿g (s ×ˢ set.univ)) :
cont_diff_on 𝕜 n (λ (q : P × G), convolution f (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}
[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]
[complete_space F]
[measurable_space G]
[normed_add_comm_group G]
[borel_space G]
[normed_space 𝕜 G]
[normed_add_comm_group P]
[normed_space 𝕜 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 : measure_theory.locally_integrable f μ)
(hg : cont_diff_on 𝕜 n ↿g (s ×ˢ set.univ)) :
cont_diff_on 𝕜 n (λ (q : P × G), convolution f (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}
[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]
[complete_space F]
[measurable_space G]
[normed_add_comm_group G]
[borel_space G]
[normed_space 𝕜 G]
[normed_add_comm_group P]
[normed_space 𝕜 P]
{μ : measure_theory.measure G}
{n : ℕ∞}
(L : E →L[𝕜] E' →L[𝕜] F)
{s : set P}
{v : P → G}
(hv : cont_diff_on 𝕜 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 : measure_theory.locally_integrable f μ)
(hg : cont_diff_on 𝕜 n ↿g (s ×ˢ set.univ)) :
cont_diff_on 𝕜 n (λ (x : P), convolution f (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}
[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]
[complete_space F]
[measurable_space G]
[normed_add_comm_group G]
[borel_space G]
[normed_space 𝕜 G]
[normed_add_comm_group P]
[normed_space 𝕜 P]
{μ : measure_theory.measure G}
[μ.is_add_left_invariant]
[μ.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 : measure_theory.locally_integrable f μ)
(hg : cont_diff_on 𝕜 n ↿g (s ×ˢ set.univ)) :
cont_diff_on 𝕜 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}
[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]
[complete_space F]
[measurable_space G]
[normed_add_comm_group G]
[borel_space G]
[normed_space 𝕜 G]
[normed_add_comm_group P]
[normed_space 𝕜 P]
{μ : measure_theory.measure G}
[μ.is_add_left_invariant]
[μ.is_neg_invariant]
(L : E' →L[𝕜] E →L[𝕜] F)
{s : set P}
{n : ℕ∞}
{v : P → G}
(hv : cont_diff_on 𝕜 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 : measure_theory.locally_integrable f μ)
(hg : cont_diff_on 𝕜 n ↿g (s ×ˢ set.univ)) :
cont_diff_on 𝕜 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}
[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]
[normed_add_comm_group G]
[borel_space G]
[normed_space 𝕜 G]
{μ : measure_theory.measure G}
(L : E →L[𝕜] E' →L[𝕜] F)
{n : ℕ∞}
(hcg : has_compact_support g)
(hf : measure_theory.locally_integrable f μ)
(hg : cont_diff 𝕜 n g) :
cont_diff 𝕜 n (convolution f g L μ)
theorem
has_compact_support.cont_diff_convolution_left
{𝕜 : Type u𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[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]
[normed_add_comm_group G]
[borel_space G]
[normed_space 𝕜 G]
{μ : measure_theory.measure G}
(L : E →L[𝕜] E' →L[𝕜] F)
[μ.is_add_left_invariant]
[μ.is_neg_invariant]
{n : ℕ∞}
(hcf : has_compact_support f)
(hf : cont_diff 𝕜 n f)
(hg : measure_theory.locally_integrable g μ) :
cont_diff 𝕜 n (convolution f g L μ)
noncomputable
def
pos_convolution
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[normed_add_comm_group E]
[normed_add_comm_group E']
[normed_add_comm_group F]
[normed_space ℝ E]
[normed_space ℝ E']
[normed_space ℝ F]
[complete_space F]
(f : ℝ → E)
(g : ℝ → E')
(L : E →L[ℝ] E' →L[ℝ] F)
(ν : measure_theory.measure ℝ . "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.
theorem
pos_convolution_eq_convolution_indicator
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[normed_add_comm_group E]
[normed_add_comm_group E']
[normed_add_comm_group F]
[normed_space ℝ E]
[normed_space ℝ E']
[normed_space ℝ F]
[complete_space F]
(f : ℝ → E)
(g : ℝ → E')
(L : E →L[ℝ] E' →L[ℝ] F)
(ν : measure_theory.measure ℝ . "volume_tac")
[measure_theory.has_no_atoms ν] :
pos_convolution f g 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}
[normed_add_comm_group E]
[normed_add_comm_group E']
[normed_add_comm_group F]
[normed_space ℝ E]
[normed_space ℝ E']
[normed_space ℝ F]
[complete_space F]
{f : ℝ → E}
{g : ℝ → E'}
{μ ν : measure_theory.measure ℝ}
[measure_theory.sigma_finite μ]
[measure_theory.sigma_finite ν]
[μ.is_add_right_invariant]
[measure_theory.has_no_atoms ν]
(hf : measure_theory.integrable_on f (set.Ioi 0) ν)
(hg : measure_theory.integrable_on g (set.Ioi 0) μ)
(L : E →L[ℝ] E' →L[ℝ] F) :
measure_theory.integrable (pos_convolution f g L ν) μ
theorem
integral_pos_convolution
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[normed_add_comm_group E]
[normed_add_comm_group E']
[normed_add_comm_group F]
[normed_space ℝ E]
[normed_space ℝ E']
[normed_space ℝ F]
[complete_space F]
[complete_space E]
[complete_space E']
{μ ν : measure_theory.measure ℝ}
[measure_theory.sigma_finite μ]
[measure_theory.sigma_finite ν]
[μ.is_add_right_invariant]
[measure_theory.has_no_atoms ν]
{f : ℝ → E}
{g : ℝ → E'}
(hf : measure_theory.integrable_on f (set.Ioi 0) ν)
(hg : measure_theory.integrable_on g (set.Ioi 0) μ)
(L : E →L[ℝ] E' →L[ℝ] F) :
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.)