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 = lmul ℝ ℝ.
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.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_of_inner.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 #
- Prove properties about the convolution if both functions are rapidly decreasing.
- Use
@[to_additive]everywhere
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) :
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) :
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
- convolution_exists_at f g x L μ = measure_theory.integrable (λ (t : G), ⇑(⇑L (f t)) (g (x - t))) μ
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
- convolution_exists f g L μ = ∀ (x : G), convolution_exists_at f g x L μ
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
measure_theory.ae_strongly_measurable.convolution_integrand'
{𝕜 : 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 μ]
(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_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]
(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_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}
(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_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
measure_theory.ae_strongly_measurable.convolution_integrand_snd
{𝕜 : 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_left_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_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_left_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
measure_theory.ae_strongly_measurable.convolution_integrand
{𝕜 : 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]
(hf : measure_theory.ae_strongly_measurable f μ)
(hg : measure_theory.ae_strongly_measurable g μ) :
theorem
measure_theory.integrable.convolution_integrand
{𝕜 : 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]
(hf : measure_theory.integrable f μ)
(hg : measure_theory.integrable g μ) :
theorem
measure_theory.integrable.ae_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]
{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.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_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]
[topological_space G]
[topological_add_group G]
[borel_space G]
[topological_space.second_countable_topology G]
[sigma_compact_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_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]
[topological_space G]
[topological_add_group G]
[borel_space G]
[topological_space.second_countable_topology G]
[sigma_compact_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_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]
[topological_space G]
[topological_add_group G]
[borel_space G]
[topological_space.second_countable_topology G]
[sigma_compact_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_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] :
convolution_exists_at g f x L.flip μ ↔ convolution_exists_at f g x L μ
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)) μ
theorem
has_compact_support.convolution_exists_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)
[measurable_space G]
{μ : measure_theory.measure G}
[add_comm_group G]
[topological_space G]
[topological_add_group G]
[borel_space G]
[topological_space.second_countable_topology G]
[μ.is_add_left_invariant]
[μ.is_neg_invariant]
[sigma_compact_space G]
(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_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]
[topological_space G]
[topological_add_group G]
[borel_space G]
[topological_space.second_countable_topology G]
[μ.is_add_left_invariant]
[μ.is_neg_invariant]
[sigma_compact_space G]
(hcg : has_compact_support g)
(hf : continuous f)
(hg : measure_theory.locally_integrable g μ) :
convolution_exists f g L μ
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)) ∂μ.
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] :
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_lmul
{𝕜 : 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.lmul 𝕜 𝕜) μ 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 μ
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
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]
[μ.is_add_left_invariant]
[μ.is_neg_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] :
function.support (convolution f g L μ) ⊆ function.support g + function.support f
theorem
has_compact_support.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]
[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
has_compact_support.continuous_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'}
[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.second_countable_topology G]
[locally_compact_space G]
[t2_space 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_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]
[topological_space G]
[topological_add_group G]
[borel_space 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
has_compact_support.continuous_convolution_right_of_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}
[normed_space ℝ F]
[complete_space F]
[add_group G]
[topological_space G]
[topological_add_group G]
[borel_space G]
[topological_space.second_countable_topology G]
(hcg : has_compact_support g)
(hf : measure_theory.integrable f μ)
(hg : continuous g) :
continuous (convolution f g L μ)
A version of has_compact_support.continuous_convolution_right that works if G is
not locally compact but requires that g is integrable.
theorem
measure_theory.integrable.integrable_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]
[topological_space G]
[topological_add_group G]
[borel_space G]
[topological_space.second_countable_topology 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
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] :
function.support (convolution f g L μ) ⊆ function.support f + function.support 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]
[topological_space G]
[topological_add_group G]
[borel_space G]
[μ.is_add_left_invariant]
[μ.is_neg_invariant] :
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]
[topological_space G]
[topological_add_group G]
[borel_space G]
[μ.is_add_left_invariant]
[μ.is_neg_invariant] :
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]
[topological_space G]
[topological_add_group G]
[borel_space G]
[μ.is_add_left_invariant]
[μ.is_neg_invariant]
{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_lmul_swap
{𝕜 : Type u_1}
{G : Type u_2}
{x : G}
[nontrivially_normed_field 𝕜]
[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]
[normed_space ℝ 𝕜]
[complete_space 𝕜]
{f g : G → 𝕜} :
convolution f g (continuous_linear_map.lmul 𝕜 𝕜) μ x = ∫ (t : G), f (x - t) * g t ∂μ
The symmetric definition of convolution where the bilinear operator is multiplication.
theorem
has_compact_support.continuous_convolution_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)
[measurable_space G]
{μ : measure_theory.measure G}
[normed_space ℝ F]
[complete_space F]
[add_comm_group G]
[topological_space G]
[topological_add_group G]
[borel_space G]
[μ.is_add_left_invariant]
[μ.is_neg_invariant]
[topological_space.second_countable_topology G]
[locally_compact_space G]
[t2_space 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_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]
[topological_space G]
[topological_add_group G]
[borel_space G]
[μ.is_add_left_invariant]
[μ.is_neg_invariant]
[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
has_compact_support.continuous_convolution_left_of_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}
[normed_space ℝ F]
[complete_space F]
[add_comm_group G]
[topological_space G]
[topological_add_group G]
[borel_space G]
[μ.is_add_left_invariant]
[μ.is_neg_invariant]
[topological_space.second_countable_topology G]
(hcf : has_compact_support f)
(hf : continuous f)
(hg : measure_theory.integrable g μ) :
continuous (convolution f g L μ)
A version of has_compact_support.continuous_convolution_left that works if G is
not locally compact but requires that g is integrable.
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₀) :
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 ε : ℝ}
(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) (g 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 assume f is integrable, but also if
L = (•) or more generally if L has a antilipschitz_with-condition.
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 ε : ℝ}
(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) (g x₀) ≤ ε) :
has_dist.dist (convolution f g (continuous_linear_map.lsmul ℝ ℝ) μ x₀) (g x₀) ≤ ε
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']
{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']
{ι : Type u_1}
{l : filter ι}
{φ : ι → G → ℝ}
(hnφ : ∀ (i : ι) (x : G), 0 ≤ φ i x)
(hiφ : ∀ (i : ι), ∫ (s : G), φ i s ∂μ = 1)
(hφ : filter.tendsto (λ (n : ι), function.support (φ n)) l (nhds 0).small_sets)
(hmg : measure_theory.ae_strongly_measurable g μ)
{x₀ : G}
(hcg : continuous_at g x₀) :
filter.tendsto (λ (i : ι), convolution (φ i) g (continuous_linear_map.lsmul ℝ ℝ) μ x₀) l (nhds (g x₀))
(φ i ⋆ g) x₀ tends to g x₀ if φ is a sequence of nonnegative functions with integral 1
whose support tends to small neighborhoods around (0 : G) and g is continuous at x₀.
See also cont_diff_bump_of_inner.convolution_tendsto_right'.
theorem
cont_diff_bump_of_inner.convolution_eq_right
{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']
{φ : cont_diff_bump_of_inner 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_of_inner.normed_convolution_eq_right
{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']
{φ : cont_diff_bump_of_inner 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_of_inner.dist_normed_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}
[normed_space ℝ E']
[inner_product_space ℝ G]
[complete_space E']
{φ : cont_diff_bump_of_inner 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_of_inner.convolution_tendsto_right'
{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))
(hmg : measure_theory.ae_strongly_measurable g μ)
{x₀ : G}
(hcg : continuous_at g x₀) :
filter.tendsto (λ (i : ι), convolution (λ (x : G), (φ i).normed μ x) g (continuous_linear_map.lsmul ℝ ℝ) μ x₀) l (nhds (g x₀))
If φ i is a sequence of normed bump function, (φ i ⋆ g) x₀ tends to g x₀ if (φ i).R
tends to 0 and g is continuous at x₀.
theorem
cont_diff_bump_of_inner.convolution_tendsto_right
{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.
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]
[has_measurable_add G]
[measure_theory.sigma_finite μ]
{ν : measure_theory.measure G}
[measure_theory.sigma_finite ν]
[ν.is_add_right_invariant]
(hL : ∀ (x : E) (y : E') (z : E''), ⇑(⇑L₂ (⇑(⇑L x) y)) z = ⇑(⇑L₃ x) (⇑(⇑L₄ y) z))
{x₀ : G}
(h₄ : convolution_exists g k L₄ ν)
(h₁ : convolution_exists f g 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.
To do: prove that hi follows from simpler conditions.
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]
[topological_space.second_countable_topology G]
[sigma_compact_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]
[topological_space.second_countable_topology G]
[sigma_compact_space G]
[measure_theory.sigma_finite μ]
[μ.is_add_left_invariant]
[normed_space 𝕜 G]
[proper_space G]
(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_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]
[topological_space.second_countable_topology G]
[sigma_compact_space G]
[measure_theory.sigma_finite μ]
[μ.is_add_left_invariant]
[normed_space 𝕜 G]
[proper_space G]
[μ.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₀
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]
[topological_space.second_countable_topology G]
[sigma_compact_space G]
[measure_theory.sigma_finite μ]
[μ.is_add_left_invariant]
[normed_space 𝕜 G]
[proper_space G]
[finite_dimensional 𝕜 G]
(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_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]
[topological_space.second_countable_topology G]
[sigma_compact_space G]
[measure_theory.sigma_finite μ]
[μ.is_add_left_invariant]
[normed_space 𝕜 G]
[proper_space G]
[finite_dimensional 𝕜 G]
[μ.is_neg_invariant]
(hcf : has_compact_support f)
(hf : cont_diff 𝕜 n f)
(hg : measure_theory.locally_integrable 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₀