Differentiability of a convolution of functions #
Criteria for a convolution of functions to be differentiable.
Main Results #
HasCompactSupport.hasFDerivAt_convolution_rightandHasCompactSupport.hasFDerivAt_convolution_left: we can compute the total derivative of the convolution as a convolution with the total derivative of the right (left) function.HasCompactSupport.contDiff_convolution_rightandHasCompactSupport.contDiff_convolution_left: the convolution is𝒞ⁿif one of the functions is𝒞ⁿwith compact support and the other function in locally integrable.
theorem
HasCompactSupport.hasFDerivAt_convolution_right
{𝕜 : Type u𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[NormedAddCommGroup E]
[NormedAddCommGroup E']
[NormedAddCommGroup F]
{f : G → E}
{g : G → E'}
[RCLike 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 E']
[NormedSpace ℝ F]
[NormedSpace 𝕜 F]
[MeasurableSpace G]
{μ : MeasureTheory.Measure G}
(L : E →L[𝕜] E' →L[𝕜] F)
[NormedAddCommGroup G]
[BorelSpace G]
[NormedSpace 𝕜 G]
[MeasureTheory.SFinite μ]
[μ.IsAddLeftInvariant]
(hcg : HasCompactSupport g)
(hf : MeasureTheory.LocallyIntegrable f μ)
(hg : ContDiff 𝕜 1 g)
(x₀ : G)
:
HasFDerivAt (MeasureTheory.convolution f g L μ)
(MeasureTheory.convolution f (fderiv 𝕜 g) (ContinuousLinearMap.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
ContinuousLinearMap.precompR.
theorem
HasCompactSupport.hasFDerivAt_convolution_left
{𝕜 : Type u𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[NormedAddCommGroup E]
[NormedAddCommGroup E']
[NormedAddCommGroup F]
{f : G → E}
{g : G → E'}
[RCLike 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 E']
[NormedSpace ℝ F]
[NormedSpace 𝕜 F]
[MeasurableSpace G]
{μ : MeasureTheory.Measure G}
(L : E →L[𝕜] E' →L[𝕜] F)
[NormedAddCommGroup G]
[BorelSpace G]
[NormedSpace 𝕜 G]
[MeasureTheory.SFinite μ]
[μ.IsAddLeftInvariant]
[μ.IsNegInvariant]
(hcf : HasCompactSupport f)
(hf : ContDiff 𝕜 1 f)
(hg : MeasureTheory.LocallyIntegrable g μ)
(x₀ : G)
:
HasFDerivAt (MeasureTheory.convolution f g L μ)
(MeasureTheory.convolution (fderiv 𝕜 f) g (ContinuousLinearMap.precompL G L) μ x₀) x₀
The one-variable case
theorem
HasCompactSupport.hasDerivAt_convolution_right
{𝕜 : Type u𝕜}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[NormedAddCommGroup E]
[NormedAddCommGroup E']
[NormedAddCommGroup F]
[RCLike 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 E']
[NormedSpace ℝ F]
[NormedSpace 𝕜 F]
{f₀ : 𝕜 → E}
{g₀ : 𝕜 → E'}
(L : E →L[𝕜] E' →L[𝕜] F)
{μ : MeasureTheory.Measure 𝕜}
[μ.IsAddLeftInvariant]
[MeasureTheory.SFinite μ]
(hf : MeasureTheory.LocallyIntegrable f₀ μ)
(hcg : HasCompactSupport g₀)
(hg : ContDiff 𝕜 1 g₀)
(x₀ : 𝕜)
:
HasDerivAt (MeasureTheory.convolution f₀ g₀ L μ) (MeasureTheory.convolution f₀ (deriv g₀) L μ x₀) x₀
theorem
HasCompactSupport.hasDerivAt_convolution_left
{𝕜 : Type u𝕜}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[NormedAddCommGroup E]
[NormedAddCommGroup E']
[NormedAddCommGroup F]
[RCLike 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 E']
[NormedSpace ℝ F]
[NormedSpace 𝕜 F]
{f₀ : 𝕜 → E}
{g₀ : 𝕜 → E'}
(L : E →L[𝕜] E' →L[𝕜] F)
{μ : MeasureTheory.Measure 𝕜}
[μ.IsAddLeftInvariant]
[MeasureTheory.SFinite μ]
[μ.IsNegInvariant]
(hcf : HasCompactSupport f₀)
(hf : ContDiff 𝕜 1 f₀)
(hg : MeasureTheory.LocallyIntegrable g₀ μ)
(x₀ : 𝕜)
:
HasDerivAt (MeasureTheory.convolution f₀ g₀ L μ) (MeasureTheory.convolution (deriv f₀) g₀ L μ x₀) x₀
theorem
MeasureTheory.hasFDerivAt_convolution_right_with_param
{𝕜 : Type u𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
{P : Type uP}
[NormedAddCommGroup E]
[NormedAddCommGroup E']
[NormedAddCommGroup F]
{f : G → E}
[RCLike 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 E']
[NormedSpace ℝ F]
[NormedSpace 𝕜 F]
[MeasurableSpace G]
[NormedAddCommGroup G]
[BorelSpace G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup P]
[NormedSpace 𝕜 P]
{μ : Measure G}
(L : E →L[𝕜] E' →L[𝕜] F)
{g : P → G → E'}
{s : Set P}
{k : Set G}
(hs : IsOpen s)
(hk : IsCompact k)
(hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0)
(hf : LocallyIntegrable f μ)
(hg : ContDiffOn 𝕜 1 (↿g) (s ×ˢ Set.univ))
(q₀ : P × G)
(hq₀ : q₀.1 ∈ s)
:
HasFDerivAt (fun (q : P × G) => convolution f (g q.1) L μ q.2)
(convolution f (fun (x : G) => fderiv 𝕜 ↿g (q₀.1, x)) (ContinuousLinearMap.precompR (P × G) L) μ q₀.2) 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
MeasureTheory.contDiffOn_convolution_right_with_param_aux
{𝕜 : Type u𝕜}
{E : Type uE}
[NormedAddCommGroup E]
[RCLike 𝕜]
[NormedSpace 𝕜 E]
{G E' F P : Type uP}
[NormedAddCommGroup E']
[NormedAddCommGroup F]
[NormedSpace 𝕜 E']
[NormedSpace ℝ F]
[NormedSpace 𝕜 F]
[MeasurableSpace G]
{μ : Measure G}
[NormedAddCommGroup G]
[BorelSpace G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup P]
[NormedSpace 𝕜 P]
{f : G → E}
{n : ℕ∞}
(L : E →L[𝕜] E' →L[𝕜] F)
{g : P → G → E'}
{s : Set P}
{k : Set G}
(hs : IsOpen s)
(hk : IsCompact k)
(hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0)
(hf : LocallyIntegrable f μ)
(hg : ContDiffOn 𝕜 (↑n) (↿g) (s ×ˢ Set.univ))
:
ContDiffOn 𝕜 (↑n) (fun (q : P × G) => convolution f (g q.1) L μ q.2) (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 contDiffOn_convolution_right_with_param, which removes this restriction.
theorem
MeasureTheory.contDiffOn_convolution_right_with_param
{𝕜 : Type u𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
{P : Type uP}
[NormedAddCommGroup E]
[NormedAddCommGroup E']
[NormedAddCommGroup F]
[RCLike 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 E']
[NormedSpace ℝ F]
[NormedSpace 𝕜 F]
[MeasurableSpace G]
[NormedAddCommGroup G]
[BorelSpace G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup P]
[NormedSpace 𝕜 P]
{μ : Measure G}
{f : G → E}
{n : ℕ∞}
(L : E →L[𝕜] E' →L[𝕜] F)
{g : P → G → E'}
{s : Set P}
{k : Set G}
(hs : IsOpen s)
(hk : IsCompact k)
(hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0)
(hf : LocallyIntegrable f μ)
(hg : ContDiffOn 𝕜 (↑n) (↿g) (s ×ˢ Set.univ))
:
ContDiffOn 𝕜 (↑n) (fun (q : P × G) => convolution f (g q.1) L μ q.2) (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
MeasureTheory.contDiffOn_convolution_right_with_param_comp
{𝕜 : Type u𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
{P : Type uP}
[NormedAddCommGroup E]
[NormedAddCommGroup E']
[NormedAddCommGroup F]
[RCLike 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 E']
[NormedSpace ℝ F]
[NormedSpace 𝕜 F]
[MeasurableSpace G]
[NormedAddCommGroup G]
[BorelSpace G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup P]
[NormedSpace 𝕜 P]
{μ : Measure G}
{n : ℕ∞}
(L : E →L[𝕜] E' →L[𝕜] F)
{s : Set P}
{v : P → G}
(hv : ContDiffOn 𝕜 (↑n) v s)
{f : G → E}
{g : P → G → E'}
{k : Set G}
(hs : IsOpen s)
(hk : IsCompact k)
(hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0)
(hf : LocallyIntegrable f μ)
(hg : ContDiffOn 𝕜 (↑n) (↿g) (s ×ˢ Set.univ))
:
ContDiffOn 𝕜 (↑n) (fun (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 C^n function.
theorem
MeasureTheory.contDiffOn_convolution_left_with_param
{𝕜 : Type u𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
{P : Type uP}
[NormedAddCommGroup E]
[NormedAddCommGroup E']
[NormedAddCommGroup F]
[RCLike 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 E']
[NormedSpace ℝ F]
[NormedSpace 𝕜 F]
[MeasurableSpace G]
[NormedAddCommGroup G]
[BorelSpace G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup P]
[NormedSpace 𝕜 P]
{μ : Measure G}
[μ.IsAddLeftInvariant]
[μ.IsNegInvariant]
(L : E' →L[𝕜] E →L[𝕜] F)
{f : G → E}
{n : ℕ∞}
{g : P → G → E'}
{s : Set P}
{k : Set G}
(hs : IsOpen s)
(hk : IsCompact k)
(hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0)
(hf : LocallyIntegrable f μ)
(hg : ContDiffOn 𝕜 (↑n) (↿g) (s ×ˢ Set.univ))
:
ContDiffOn 𝕜 (↑n) (fun (q : P × G) => convolution (g q.1) f L μ q.2) (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
MeasureTheory.contDiffOn_convolution_left_with_param_comp
{𝕜 : Type u𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
{P : Type uP}
[NormedAddCommGroup E]
[NormedAddCommGroup E']
[NormedAddCommGroup F]
[RCLike 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 E']
[NormedSpace ℝ F]
[NormedSpace 𝕜 F]
[MeasurableSpace G]
[NormedAddCommGroup G]
[BorelSpace G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup P]
[NormedSpace 𝕜 P]
{μ : Measure G}
[μ.IsAddLeftInvariant]
[μ.IsNegInvariant]
(L : E' →L[𝕜] E →L[𝕜] F)
{s : Set P}
{n : ℕ∞}
{v : P → G}
(hv : ContDiffOn 𝕜 (↑n) v s)
{f : G → E}
{g : P → G → E'}
{k : Set G}
(hs : IsOpen s)
(hk : IsCompact k)
(hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0)
(hf : LocallyIntegrable f μ)
(hg : ContDiffOn 𝕜 (↑n) (↿g) (s ×ˢ Set.univ))
:
ContDiffOn 𝕜 (↑n) (fun (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 C^n functions.
theorem
HasCompactSupport.contDiff_convolution_right
{𝕜 : Type u𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[NormedAddCommGroup E]
[NormedAddCommGroup E']
[NormedAddCommGroup F]
{f : G → E}
{g : G → E'}
[RCLike 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 E']
[NormedSpace ℝ F]
[NormedSpace 𝕜 F]
[MeasurableSpace G]
[NormedAddCommGroup G]
[BorelSpace G]
[NormedSpace 𝕜 G]
{μ : MeasureTheory.Measure G}
(L : E →L[𝕜] E' →L[𝕜] F)
{n : ℕ∞}
(hcg : HasCompactSupport g)
(hf : MeasureTheory.LocallyIntegrable f μ)
(hg : ContDiff 𝕜 (↑n) g)
:
ContDiff 𝕜 (↑n) (MeasureTheory.convolution f g L μ)
theorem
HasCompactSupport.contDiff_convolution_left
{𝕜 : Type u𝕜}
{G : Type uG}
{E : Type uE}
{E' : Type uE'}
{F : Type uF}
[NormedAddCommGroup E]
[NormedAddCommGroup E']
[NormedAddCommGroup F]
{f : G → E}
{g : G → E'}
[RCLike 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 E']
[NormedSpace ℝ F]
[NormedSpace 𝕜 F]
[MeasurableSpace G]
[NormedAddCommGroup G]
[BorelSpace G]
[NormedSpace 𝕜 G]
{μ : MeasureTheory.Measure G}
(L : E →L[𝕜] E' →L[𝕜] F)
[μ.IsAddLeftInvariant]
[μ.IsNegInvariant]
{n : ℕ∞}
(hcf : HasCompactSupport f)
(hf : ContDiff 𝕜 (↑n) f)
(hg : MeasureTheory.LocallyIntegrable g μ)
:
ContDiff 𝕜 (↑n) (MeasureTheory.convolution f g L μ)