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

We also define ConvolutionExists and ConvolutionExistsAt to state that the convolution is well-defined (everywhere or at a single point). These conditions are needed for pointwise computations (e.g. ConvolutionExistsAt.distrib_add), but are generally not strong 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 HasCompactSupport.hasFDerivAt_convolution_right.
• This allows us to use @[to_additive] everywhere (which would not be possible if we would use mul/smul in the integral, since @[to_additive] will incorrectly also try to additivize those definitions).
• We need to support the case where at least one of the functions is vector-valued, but if we use smul to multiply the functions, that would be an asymmetric definition.

Main Definitions

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

Main Results

• HasCompactSupport.hasFDerivAt_convolution_right and HasCompactSupport.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_right and HasCompactSupport.contDiff_convolution_left: the convolution is 𝒞ⁿ if one of the functions is 𝒞ⁿ with compact support and the other function in locally integrable.

Versions of these statements for functions depending on a parameter are also given.

• convolution_tendsto_right: Given a sequence of nonnegative normalized functions whose support tends to a small neighborhood around 0, the convolution tends to the right argument. This is specialized to bump functions in ContDiffBump.convolution_tendsto_right.

Notation

The following notations are localized in the locale convolution:

• f ⋆[L, μ] g for the convolution. Note: you have to use parentheses to apply the convolution to an argument: (f ⋆[L, μ] g) x.
• f ⋆[L] g := f ⋆[L, volume] g
• f ⋆ g := f ⋆[lsmul ℝ ℝ] g

To do

• Existence and (uniform) continuity of the convolution if one of the maps is in ℒ^p and the other in ℒ^q with 1 / p + 1 / q = 1. This might require a generalization of MeasureTheory.Memℒp.smul where smul is generalized to a continuous bilinear map. (see e.g. [Fremlin, Measure Theory (volume 2)][fremlin_vol2], 255K)
• The convolution is an AEStronglyMeasurable function (see e.g. [Fremlin, Measure Theory (volume 2)][fremlin_vol2], 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} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : G → E} {g : G → E'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [AddGroup G] [TopologicalSpace G] {C : ℝ} (hC : ∀ (i : G), ‖g i‖ ≤ C) {x : G} {t : G} {s : Set G} {u : Set G} (hx : x ∈ s) (hu : -tsupport g + s ⊆ u) : ‖(L (f t)) (g (x - t))‖ ≤ Set.indicator u (fun (t : G) => ‖L‖ * ‖f t‖ * C) t

theorem HasCompactSupport.convolution_integrand_bound_right_of_subset {𝕜 : 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'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [AddGroup G] [TopologicalSpace G] (hcg : HasCompactSupport g) (hg : Continuous g) {x : G} {t : G} {s : Set G} {u : Set G} (hx : x ∈ s) (hu : -tsupport g + s ⊆ u) : ‖(L (f t)) (g (x - t))‖ ≤ Set.indicator u (fun (t : G) => ‖L‖ * ‖f t‖ * ⨆ (i : G), ‖g i‖) t

theorem HasCompactSupport.convolution_integrand_bound_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'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [AddGroup G] [TopologicalSpace G] (hcg : HasCompactSupport g) (hg : Continuous g) {x : G} {t : G} {s : Set G} (hx : x ∈ s) : ‖(L (f t)) (g (x - t))‖ ≤ Set.indicator (-tsupport g + s) (fun (t : G) => ‖L‖ * ‖f t‖ * ⨆ (i : G), ‖g i‖) t

theorem Continuous.convolution_integrand_fst {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : G → E} {g : G → E'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [AddGroup G] [TopologicalSpace G] [ContinuousSub G] (hg : Continuous g) (t : G) : Continuous fun (x : G) => (L (f t)) (g (x - t))

theorem HasCompactSupport.convolution_integrand_bound_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'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [AddGroup G] [TopologicalSpace G] (hcf : HasCompactSupport f) (hf : Continuous f) {x : G} {t : G} {s : Set G} (hx : x ∈ s) : ‖(L (f (x - t))) (g t)‖ ≤ Set.indicator (-tsupport f + s) (fun (t : G) => (‖L‖ * ⨆ (i : G), ‖f i‖) * ‖g t‖) t

def ConvolutionExistsAt {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] [MeasurableSpace G] [Sub G] (f : G → E) (g : G → E') (x : G) (L : E →L[𝕜] E' →L[𝕜] F) (μ : autoParam (MeasureTheory.Measure G) _auto✝) : 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

• ConvolutionExistsAt f g x L = MeasureTheory.Integrable fun (t : G) => (L (f t)) (g (x - t))

def ConvolutionExists {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] [MeasurableSpace G] [Sub G] (f : G → E) (g : G → E') (L : E →L[𝕜] E' →L[𝕜] F) (μ : autoParam (MeasureTheory.Measure G) _auto✝) : 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

• ConvolutionExists f g L = ∀ (x : G), ConvolutionExistsAt f g x L

theorem ConvolutionExistsAt.integrable {𝕜 : 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'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] {L : E →L[𝕜] E' →L[𝕜] F} [MeasurableSpace G] {μ : MeasureTheory.Measure G} [Sub G] {x : G} (h : ConvolutionExistsAt f g x L) : MeasureTheory.Integrable fun (t : G) => (L (f t)) (g (x - t))

theorem MeasureTheory.AEStronglyMeasurable.convolution_integrand' {𝕜 : 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'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} {ν : MeasureTheory.Measure G} [AddGroup G] [MeasurableAdd₂ G] [MeasurableNeg G] [MeasureTheory.SigmaFinite ν] (hf : MeasureTheory.AEStronglyMeasurable f ν) (hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map (fun (p : G × G) => p.1 - p.2) (MeasureTheory.Measure.prod μ ν))) : MeasureTheory.AEStronglyMeasurable (fun (p : G × G) => (L (f p.2)) (g (p.1 - p.2))) (MeasureTheory.Measure.prod μ ν)

theorem MeasureTheory.AEStronglyMeasurable.convolution_integrand_snd' {𝕜 : 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'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} [AddGroup G] [MeasurableAdd G] [MeasurableNeg G] (hf : MeasureTheory.AEStronglyMeasurable f μ) {x : G} (hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map (fun (t : G) => x - t) μ)) : MeasureTheory.AEStronglyMeasurable (fun (t : G) => (L (f t)) (g (x - t))) μ

theorem MeasureTheory.AEStronglyMeasurable.convolution_integrand_swap_snd' {𝕜 : 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'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} [AddGroup G] [MeasurableAdd G] [MeasurableNeg G] {x : G} (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map (fun (t : G) => x - t) μ)) (hg : MeasureTheory.AEStronglyMeasurable g μ) : MeasureTheory.AEStronglyMeasurable (fun (t : G) => (L (f (x - t))) (g t)) μ

theorem BddAbove.convolutionExistsAt' {𝕜 : 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'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} [AddGroup G] [MeasurableAdd G] [MeasurableNeg G] {x₀ : G} {s : Set G} (hbg : BddAbove ((fun (i : G) => ‖g i‖) '' ((fun (t : G) => -t + x₀) ⁻¹' s))) (hs : MeasurableSet s) (h2s : (Function.support fun (t : G) => (L (f t)) (g (x₀ - t))) ⊆ s) (hf : MeasureTheory.IntegrableOn f s) (hmg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map (fun (t : G) => x₀ - t) (MeasureTheory.Measure.restrict μ s))) : ConvolutionExistsAt 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 ConvolutionExistsAt.ofNorm' {𝕜 : 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'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} [AddGroup G] [MeasurableAdd G] [MeasurableNeg G] {x₀ : G} (h : ConvolutionExistsAt (fun (x : G) => ‖f x‖) (fun (x : G) => ‖g x‖) x₀ (ContinuousLinearMap.mul ℝ ℝ)) (hmf : MeasureTheory.AEStronglyMeasurable f μ) (hmg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map (fun (t : G) => x₀ - t) μ)) : ConvolutionExistsAt f g x₀ L

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

theorem MeasureTheory.AEStronglyMeasurable.convolution_integrand_snd {𝕜 : 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'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} [AddGroup G] [MeasurableAdd₂ G] [MeasurableNeg G] [MeasureTheory.SigmaFinite μ] [MeasureTheory.Measure.IsAddRightInvariant μ] (hf : MeasureTheory.AEStronglyMeasurable f μ) (hg : MeasureTheory.AEStronglyMeasurable g μ) (x : G) : MeasureTheory.AEStronglyMeasurable (fun (t : G) => (L (f t)) (g (x - t))) μ

theorem MeasureTheory.AEStronglyMeasurable.convolution_integrand_swap_snd {𝕜 : 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'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} [AddGroup G] [MeasurableAdd₂ G] [MeasurableNeg G] [MeasureTheory.SigmaFinite μ] [MeasureTheory.Measure.IsAddRightInvariant μ] (hf : MeasureTheory.AEStronglyMeasurable f μ) (hg : MeasureTheory.AEStronglyMeasurable g μ) (x : G) : MeasureTheory.AEStronglyMeasurable (fun (t : G) => (L (f (x - t))) (g t)) μ

theorem ConvolutionExistsAt.ofNorm {𝕜 : 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'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} [AddGroup G] [MeasurableAdd₂ G] [MeasurableNeg G] [MeasureTheory.SigmaFinite μ] [MeasureTheory.Measure.IsAddRightInvariant μ] {x₀ : G} (h : ConvolutionExistsAt (fun (x : G) => ‖f x‖) (fun (x : G) => ‖g x‖) x₀ (ContinuousLinearMap.mul ℝ ℝ)) (hmf : MeasureTheory.AEStronglyMeasurable f μ) (hmg : MeasureTheory.AEStronglyMeasurable g μ) : ConvolutionExistsAt f g x₀ L

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

theorem MeasureTheory.AEStronglyMeasurable.convolution_integrand {𝕜 : 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'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} {ν : MeasureTheory.Measure G} [AddGroup G] [MeasurableAdd₂ G] [MeasurableNeg G] [MeasureTheory.SigmaFinite μ] [MeasureTheory.Measure.IsAddRightInvariant μ] [MeasureTheory.SigmaFinite ν] (hf : MeasureTheory.AEStronglyMeasurable f ν) (hg : MeasureTheory.AEStronglyMeasurable g μ) : MeasureTheory.AEStronglyMeasurable (fun (p : G × G) => (L (f p.2)) (g (p.1 - p.2))) (MeasureTheory.Measure.prod μ ν)

theorem MeasureTheory.Integrable.convolution_integrand {𝕜 : 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'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} {ν : MeasureTheory.Measure G} [AddGroup G] [MeasurableAdd₂ G] [MeasurableNeg G] [MeasureTheory.SigmaFinite μ] [MeasureTheory.Measure.IsAddRightInvariant μ] [MeasureTheory.SigmaFinite ν] (hf : MeasureTheory.Integrable f) (hg : MeasureTheory.Integrable g) : MeasureTheory.Integrable fun (p : G × G) => (L (f p.2)) (g (p.1 - p.2))

theorem MeasureTheory.Integrable.ae_convolution_exists {𝕜 : 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'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} {ν : MeasureTheory.Measure G} [AddGroup G] [MeasurableAdd₂ G] [MeasurableNeg G] [MeasureTheory.SigmaFinite μ] [MeasureTheory.Measure.IsAddRightInvariant μ] [MeasureTheory.SigmaFinite ν] (hf : MeasureTheory.Integrable f) (hg : MeasureTheory.Integrable g) : ∀ᵐ (x : G) ∂μ, ConvolutionExistsAt f g x L

theorem HasCompactSupport.convolutionExistsAt {𝕜 : 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'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [BorelSpace G] {x₀ : G} (h : HasCompactSupport fun (t : G) => (L (f t)) (g (x₀ - t))) (hf : MeasureTheory.LocallyIntegrable f) (hg : Continuous g) : ConvolutionExistsAt f g x₀ L

theorem HasCompactSupport.convolutionExists_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'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [BorelSpace G] (hcg : HasCompactSupport g) (hf : MeasureTheory.LocallyIntegrable f) (hg : Continuous g) : ConvolutionExists f g L

theorem HasCompactSupport.convolutionExists_left_of_continuous_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'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [BorelSpace G] (hcf : HasCompactSupport f) (hf : MeasureTheory.LocallyIntegrable f) (hg : Continuous g) : ConvolutionExists f g L

theorem BddAbove.convolutionExistsAt {𝕜 : 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'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} [AddCommGroup G] [MeasurableNeg G] [MeasureTheory.Measure.IsAddLeftInvariant μ] [MeasurableAdd₂ G] [MeasureTheory.SigmaFinite μ] {x₀ : G} {s : Set G} (hbg : BddAbove ((fun (i : G) => ‖g i‖) '' ((fun (t : G) => x₀ - t) ⁻¹' s))) (hs : MeasurableSet s) (h2s : (Function.support fun (t : G) => (L (f t)) (g (x₀ - t))) ⊆ s) (hf : MeasureTheory.IntegrableOn f s) (hmg : MeasureTheory.AEStronglyMeasurable g μ) : ConvolutionExistsAt 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 BddAbove.convolutionExistsAt' 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 convolutionExistsAt_flip {𝕜 : 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'} {x : G} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] {L : E →L[𝕜] E' →L[𝕜] F} [MeasurableSpace G] {μ : MeasureTheory.Measure G} [AddCommGroup G] [MeasurableNeg G] [MeasureTheory.Measure.IsAddLeftInvariant μ] [MeasurableAdd G] [MeasureTheory.Measure.IsNegInvariant μ] : ConvolutionExistsAt g f x (ContinuousLinearMap.flip L) ↔ ConvolutionExistsAt f g x L

theorem ConvolutionExistsAt.integrable_swap {𝕜 : 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'} {x : G} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] {L : E →L[𝕜] E' →L[𝕜] F} [MeasurableSpace G] {μ : MeasureTheory.Measure G} [AddCommGroup G] [MeasurableNeg G] [MeasureTheory.Measure.IsAddLeftInvariant μ] [MeasurableAdd G] [MeasureTheory.Measure.IsNegInvariant μ] (h : ConvolutionExistsAt f g x L) : MeasureTheory.Integrable fun (t : G) => (L (f (x - t))) (g t)

theorem convolutionExistsAt_iff_integrable_swap {𝕜 : 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'} {x : G} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] {L : E →L[𝕜] E' →L[𝕜] F} [MeasurableSpace G] {μ : MeasureTheory.Measure G} [AddCommGroup G] [MeasurableNeg G] [MeasureTheory.Measure.IsAddLeftInvariant μ] [MeasurableAdd G] [MeasureTheory.Measure.IsNegInvariant μ] : ConvolutionExistsAt f g x L ↔ MeasureTheory.Integrable fun (t : G) => (L (f (x - t))) (g t)

theorem HasCompactSupport.convolutionExistsLeft {𝕜 : 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'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} [AddCommGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [BorelSpace G] [MeasureTheory.Measure.IsAddLeftInvariant μ] [MeasureTheory.Measure.IsNegInvariant μ] (hcf : HasCompactSupport f) (hf : Continuous f) (hg : MeasureTheory.LocallyIntegrable g) : ConvolutionExists f g L

theorem HasCompactSupport.convolutionExistsRightOfContinuousLeft {𝕜 : 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'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} [AddCommGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [BorelSpace G] [MeasureTheory.Measure.IsAddLeftInvariant μ] [MeasureTheory.Measure.IsNegInvariant μ] (hcg : HasCompactSupport g) (hf : Continuous f) (hg : MeasureTheory.LocallyIntegrable g) : ConvolutionExists f g L

noncomputable def convolution {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] [MeasurableSpace G] [NormedSpace ℝ F] [Sub G] (f : G → E) (g : G → E') (L : E →L[𝕜] E' →L[𝕜] F) (μ : autoParam (MeasureTheory.Measure G) _auto✝) : G → F

The convolution of two functions f and g with respect to a continuous bilinear map L and measure μ. It is defined to be (f ⋆[L, μ] g) x = ∫ t, L (f t) (g (x - t)) ∂μ.

Equations

• convolution f g L x = ∫ (t : G), (L (f t)) (g (x - t)) ∂μ

def Convolution.«term_⋆[_,_]_» : Lean.TrailingParserDescr

The convolution of two functions with respect to a bilinear operation L and a measure μ.

Equations

• One or more equations did not get rendered due to their size.

def Convolution.«term_⋆[_]_» : Lean.TrailingParserDescr

The convolution of two functions with respect to a bilinear operation L and the volume.

Equations

• One or more equations did not get rendered due to their size.

def Convolution.«term_⋆_» : Lean.TrailingParserDescr

The convolution of two real-valued functions with respect to volume.

Equations

• Convolution.«term_⋆_» = Lean.ParserDescr.trailingNode `Convolution.term_⋆_ 67 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⋆ ") (Lean.ParserDescr.cat `term 66))

theorem convolution_def {𝕜 : 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'} {x : G} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace ℝ F] [Sub G] : convolution f g L x = ∫ (t : G), (L (f t)) (g (x - t)) ∂μ

theorem convolution_lsmul {𝕜 : Type u𝕜} {G : Type uG} {F : Type uF} [NormedAddCommGroup F] {x : G} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 F] [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace ℝ F] [Sub G] {f : G → 𝕜} {g : G → F} : convolution f g (ContinuousLinearMap.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} [NontriviallyNormedField 𝕜] [MeasurableSpace G] {μ : MeasureTheory.Measure G} [Sub G] [NormedSpace ℝ 𝕜] {f : G → 𝕜} {g : G → 𝕜} : convolution f g (ContinuousLinearMap.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} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : G → E} {g : G → E'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] {L : E →L[𝕜] E' →L[𝕜] F} [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace ℝ F] [AddGroup G] [SMulCommClass ℝ 𝕜 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} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : G → E} {g : G → E'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] {L : E →L[𝕜] E' →L[𝕜] F} [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace ℝ F] [AddGroup G] [SMulCommClass ℝ 𝕜 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} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {g : G → E'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] {L : E →L[𝕜] E' →L[𝕜] F} [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace ℝ F] [AddGroup G] : convolution 0 g L = 0

@[simp]

theorem convolution_zero {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : G → E} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] {L : E →L[𝕜] E' →L[𝕜] F} [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace ℝ F] [AddGroup G] : convolution f 0 L = 0

theorem ConvolutionExistsAt.distrib_add {𝕜 : 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'} {g' : G → E'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] {L : E →L[𝕜] E' →L[𝕜] F} [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace ℝ F] [AddGroup G] {x : G} (hfg : ConvolutionExistsAt f g x L) (hfg' : ConvolutionExistsAt f g' x L) : convolution f (g + g') L x = convolution f g L x + convolution f g' L x

theorem ConvolutionExists.distrib_add {𝕜 : 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'} {g' : G → E'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] {L : E →L[𝕜] E' →L[𝕜] F} [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace ℝ F] [AddGroup G] (hfg : ConvolutionExists f g L) (hfg' : ConvolutionExists f g' L) : convolution f (g + g') L = convolution f g L + convolution f g' L

theorem ConvolutionExistsAt.add_distrib {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : G → E} {f' : G → E} {g : G → E'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] {L : E →L[𝕜] E' →L[𝕜] F} [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace ℝ F] [AddGroup G] {x : G} (hfg : ConvolutionExistsAt f g x L) (hfg' : ConvolutionExistsAt f' g x L) : convolution (f + f') g L x = convolution f g L x + convolution f' g L x

theorem ConvolutionExists.add_distrib {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : G → E} {f' : G → E} {g : G → E'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] {L : E →L[𝕜] E' →L[𝕜] F} [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace ℝ F] [AddGroup G] (hfg : ConvolutionExists f g L) (hfg' : ConvolutionExists 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} [MeasurableSpace G] {μ : MeasureTheory.Measure G} [AddGroup G] {f : G → ℝ} {g : G → ℝ} {g' : G → ℝ} (hfg : ConvolutionExistsAt f g x (ContinuousLinearMap.lsmul ℝ ℝ)) (hfg' : ConvolutionExistsAt f g' x (ContinuousLinearMap.lsmul ℝ ℝ)) (hf : ∀ (x : G), 0 ≤ f x) (hg : ∀ (x : G), g x ≤ g' x) : convolution f g (ContinuousLinearMap.lsmul ℝ ℝ) x ≤ convolution f g' (ContinuousLinearMap.lsmul ℝ ℝ) x

theorem convolution_mono_right_of_nonneg {G : Type uG} {x : G} [MeasurableSpace G] {μ : MeasureTheory.Measure G} [AddGroup G] {f : G → ℝ} {g : G → ℝ} {g' : G → ℝ} (hfg' : ConvolutionExistsAt f g' x (ContinuousLinearMap.lsmul ℝ ℝ)) (hf : ∀ (x : G), 0 ≤ f x) (hg : ∀ (x : G), g x ≤ g' x) (hg' : ∀ (x : G), 0 ≤ g' x) : convolution f g (ContinuousLinearMap.lsmul ℝ ℝ) x ≤ convolution f g' (ContinuousLinearMap.lsmul ℝ ℝ) x

theorem convolution_congr {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : G → E} {f' : G → E} {g : G → E'} {g' : G → E'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace ℝ F] [AddGroup G] [MeasurableAdd₂ G] [MeasurableNeg G] [MeasureTheory.SigmaFinite μ] [MeasureTheory.Measure.IsAddRightInvariant μ] (h1 : f =ᶠ[MeasureTheory.Measure.ae μ] f') (h2 : g =ᶠ[MeasureTheory.Measure.ae μ] 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} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : G → E} {g : G → E'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace ℝ F] [AddGroup G] : Function.support (convolution f g L) ⊆ Function.support g + Function.support f

theorem MeasureTheory.Integrable.integrable_convolution {𝕜 : 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'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace ℝ F] [AddGroup G] [MeasurableAdd₂ G] [MeasurableNeg G] [MeasureTheory.SigmaFinite μ] [MeasureTheory.Measure.IsAddRightInvariant μ] (hf : MeasureTheory.Integrable f) (hg : MeasureTheory.Integrable g) : MeasureTheory.Integrable (convolution f g L)

theorem HasCompactSupport.convolution {𝕜 : 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'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace ℝ F] [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [T2Space G] (hcf : HasCompactSupport f) (hcg : HasCompactSupport g) : HasCompactSupport (convolution f g L)

theorem continuousOn_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} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace ℝ F] [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [BorelSpace G] [TopologicalSpace P] {g : P → G → E'} {s : Set P} {k : Set G} (hk : IsCompact k) (hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0) (hf : MeasureTheory.LocallyIntegrable f) (hg : ContinuousOn (↿g) (s ×ˢ Set.univ)) : ContinuousOn (fun (q : P × G) => convolution f (g q.1) L q.2) (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 continuousOn_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] {f : G → E} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace ℝ F] [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [BorelSpace G] [TopologicalSpace P] {s : Set P} {v : P → G} (hv : ContinuousOn v s) {g : P → G → E'} {k : Set G} (hk : IsCompact k) (hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0) (hf : MeasureTheory.LocallyIntegrable f) (hg : ContinuousOn (↿g) (s ×ˢ Set.univ)) : ContinuousOn (fun (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 HasCompactSupport.continuous_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'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace ℝ F] [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [BorelSpace G] (hcg : HasCompactSupport g) (hf : MeasureTheory.LocallyIntegrable 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 BddAbove.continuous_convolution_right_of_integrable {𝕜 : 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'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace ℝ F] [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [BorelSpace G] [FirstCountableTopology G] [SecondCountableTopologyEither G E'] (hbg : BddAbove (Set.range fun (x : G) => ‖g x‖)) (hf : MeasureTheory.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} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : G → E} {g : G → E'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace ℝ F] [AddCommGroup 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} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : G → E} {g : G → E'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace ℝ F] [AddCommGroup G] [MeasureTheory.Measure.IsAddLeftInvariant μ] [MeasureTheory.Measure.IsNegInvariant μ] [MeasurableNeg G] [MeasurableAdd G] : convolution g f (ContinuousLinearMap.flip L) = 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} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : G → E} {g : G → E'} {x : G} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace ℝ F] [AddCommGroup G] [MeasureTheory.Measure.IsAddLeftInvariant μ] [MeasureTheory.Measure.IsNegInvariant μ] [MeasurableNeg G] [MeasurableAdd G] : convolution f g L x = ∫ (t : G), (L (f (x - t))) (g t) ∂μ

The symmetric definition of convolution.

theorem convolution_lsmul_swap {𝕜 : Type u𝕜} {G : Type uG} {F : Type uF} [NormedAddCommGroup F] {x : G} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 F] [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace ℝ F] [AddCommGroup G] [MeasureTheory.Measure.IsAddLeftInvariant μ] [MeasureTheory.Measure.IsNegInvariant μ] [MeasurableNeg G] [MeasurableAdd G] {f : G → 𝕜} {g : G → F} : convolution f g (ContinuousLinearMap.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} [NontriviallyNormedField 𝕜] [MeasurableSpace G] {μ : MeasureTheory.Measure G} [AddCommGroup G] [MeasureTheory.Measure.IsAddLeftInvariant μ] [MeasureTheory.Measure.IsNegInvariant μ] [MeasurableNeg G] [MeasurableAdd G] [NormedSpace ℝ 𝕜] {f : G → 𝕜} {g : G → 𝕜} : convolution f g (ContinuousLinearMap.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} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : G → E} {g : G → E'} {x : G} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace ℝ F] [AddCommGroup G] [MeasureTheory.Measure.IsAddLeftInvariant μ] [MeasureTheory.Measure.IsNegInvariant μ] [MeasurableNeg G] [MeasurableAdd 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 HasCompactSupport.continuous_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'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace ℝ F] [AddCommGroup G] [MeasureTheory.Measure.IsAddLeftInvariant μ] [MeasureTheory.Measure.IsNegInvariant μ] [TopologicalSpace G] [TopologicalAddGroup G] [BorelSpace G] (hcf : HasCompactSupport f) (hf : Continuous f) (hg : MeasureTheory.LocallyIntegrable g) : Continuous (convolution f g L)

theorem BddAbove.continuous_convolution_left_of_integrable {𝕜 : 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'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace ℝ F] [AddCommGroup G] [MeasureTheory.Measure.IsAddLeftInvariant μ] [MeasureTheory.Measure.IsNegInvariant μ] [TopologicalSpace G] [TopologicalAddGroup G] [BorelSpace G] [FirstCountableTopology G] [SecondCountableTopologyEither G E] (hbf : BddAbove (Set.range fun (x : G) => ‖f x‖)) (hf : Continuous f) (hg : MeasureTheory.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} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : G → E} {g : G → E'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace ℝ F] [SeminormedAddCommGroup G] {x₀ : G} {R : ℝ} (hf : Function.support f ⊆ Metric.ball 0 R) (hg : ∀ x ∈ Metric.ball x₀ R, g x = g x₀) : convolution f g L x₀ = ∫ (t : G), (L (f t)) (g x₀) ∂μ

Compute (f ⋆ g) x₀ if the support of the f is within Metric.ball 0 R, and g is constant on Metric.ball x₀ R.

We can simplify the RHS further if we assume f is integrable, but also if L = (•) or more generally if L has an AntilipschitzWith-condition.

theorem dist_convolution_le' {𝕜 : 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'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace ℝ F] [SeminormedAddCommGroup G] [BorelSpace G] [SecondCountableTopology G] [MeasureTheory.Measure.IsAddLeftInvariant μ] [MeasureTheory.SigmaFinite μ] {x₀ : G} {R : ℝ} {ε : ℝ} {z₀ : E'} (hε : 0 ≤ ε) (hif : MeasureTheory.Integrable f) (hf : Function.support f ⊆ Metric.ball 0 R) (hmg : MeasureTheory.AEStronglyMeasurable g μ) (hg : ∀ x ∈ Metric.ball x₀ R, dist (g x) z₀ ≤ ε) : dist (convolution f g L x₀) (∫ (t : G), (L (f t)) z₀ ∂μ) ≤ (‖L‖ * ∫ (x : G), ‖f x‖ ∂μ) * ε

Approximate (f ⋆ g) x₀ if the support of the f is bounded within a ball, and g is near g x₀ on a ball with the same radius around x₀. See dist_convolution_le for a special case.

We can simplify the second argument of dist further if we add some extra type-classes on E and 𝕜 or if L is scalar multiplication.

theorem dist_convolution_le {G : Type uG} {E' : Type uE'} [NormedAddCommGroup E'] {g : G → E'} [MeasurableSpace G] {μ : MeasureTheory.Measure G} [SeminormedAddCommGroup G] [BorelSpace G] [SecondCountableTopology G] [MeasureTheory.Measure.IsAddLeftInvariant μ] [MeasureTheory.SigmaFinite μ] [NormedSpace ℝ E'] [CompleteSpace 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 : MeasureTheory.AEStronglyMeasurable g μ) (hg : ∀ x ∈ Metric.ball x₀ R, dist (g x) z₀ ≤ ε) : dist (convolution f g (ContinuousLinearMap.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'} [NormedAddCommGroup E'] [MeasurableSpace G] {μ : MeasureTheory.Measure G} [SeminormedAddCommGroup G] [BorelSpace G] [SecondCountableTopology G] [MeasureTheory.Measure.IsAddLeftInvariant μ] [MeasureTheory.SigmaFinite μ] [NormedSpace ℝ E'] [CompleteSpace 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 (fun (n : ι) => Function.support (φ n)) l (Filter.smallSets (nhds 0))) (hmg : ∀ᶠ (i : ι) in l, MeasureTheory.AEStronglyMeasurable (g i) μ) (hcg : Filter.Tendsto (Function.uncurry g) (l ×ˢ nhds x₀) (nhds z₀)) (hk : Filter.Tendsto k l (nhds x₀)) : Filter.Tendsto (fun (i : ι) => convolution (φ i) (g i) (ContinuousLinearMap.lsmul ℝ ℝ) (k i)) l (nhds z₀)

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

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

See also ContDiffBump.convolution_tendsto_right.

theorem integral_convolution {𝕜 : 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'} [IsROrC 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [CompleteSpace F] [MeasurableSpace G] {μ : MeasureTheory.Measure G} {ν : MeasureTheory.Measure G} (L : E →L[𝕜] E' →L[𝕜] F) [AddGroup G] [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] [MeasureTheory.Measure.IsAddRightInvariant μ] [MeasurableAdd₂ G] [MeasurableNeg G] [NormedSpace ℝ E] [NormedSpace ℝ E'] [CompleteSpace E] [CompleteSpace E'] (hf : MeasureTheory.Integrable f) (hg : MeasureTheory.Integrable g) : ∫ (x : G), convolution f g L x ∂μ = (L (∫ (x : G), f x ∂ν)) (∫ (x : G), g x ∂μ)

theorem convolution_assoc' {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {E'' : Type uE''} {F : Type uF} {F' : Type uF'} {F'' : Type uF''} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup E''] [NormedAddCommGroup F] {f : G → E} {g : G → E'} [IsROrC 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 E''] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [CompleteSpace F] [MeasurableSpace G] {μ : MeasureTheory.Measure G} {ν : MeasureTheory.Measure G} (L : E →L[𝕜] E' →L[𝕜] F) [NormedAddCommGroup F'] [NormedSpace ℝ F'] [NormedSpace 𝕜 F'] [CompleteSpace F'] [NormedAddCommGroup F''] [NormedSpace ℝ F''] [NormedSpace 𝕜 F''] [CompleteSpace F''] {k : G → E''} (L₂ : F →L[𝕜] E'' →L[𝕜] F') (L₃ : E →L[𝕜] F'' →L[𝕜] F') (L₄ : E' →L[𝕜] E'' →L[𝕜] F'') [AddGroup G] [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] [MeasureTheory.Measure.IsAddRightInvariant μ] [MeasurableAdd₂ G] [MeasureTheory.Measure.IsAddRightInvariant ν] [MeasurableNeg G] (hL : ∀ (x : E) (y : E') (z : E''), (L₂ ((L x) y)) z = (L₃ x) ((L₄ y) z)) {x₀ : G} (hfg : ∀ᵐ (y : G) ∂μ, ConvolutionExistsAt f g y L) (hgk : ∀ᵐ (x : G) ∂ν, ConvolutionExistsAt g k x L₄) (hi : MeasureTheory.Integrable (Function.uncurry fun (x y : G) => (L₃ (f y)) ((L₄ (g (x - y))) (k (x₀ - x))))) : 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''} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup E''] [NormedAddCommGroup F] {f : G → E} {g : G → E'} [IsROrC 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 E''] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [CompleteSpace F] [MeasurableSpace G] {μ : MeasureTheory.Measure G} {ν : MeasureTheory.Measure G} (L : E →L[𝕜] E' →L[𝕜] F) [NormedAddCommGroup F'] [NormedSpace ℝ F'] [NormedSpace 𝕜 F'] [CompleteSpace F'] [NormedAddCommGroup F''] [NormedSpace ℝ F''] [NormedSpace 𝕜 F''] [CompleteSpace F''] {k : G → E''} (L₂ : F →L[𝕜] E'' →L[𝕜] F') (L₃ : E →L[𝕜] F'' →L[𝕜] F') (L₄ : E' →L[𝕜] E'' →L[𝕜] F'') [AddGroup G] [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] [MeasureTheory.Measure.IsAddRightInvariant μ] [MeasurableAdd₂ G] [MeasureTheory.Measure.IsAddRightInvariant ν] [MeasurableNeg G] (hL : ∀ (x : E) (y : E') (z : E''), (L₂ ((L x) y)) z = (L₃ x) ((L₄ y) z)) {x₀ : G} (hf : MeasureTheory.AEStronglyMeasurable f ν) (hg : MeasureTheory.AEStronglyMeasurable g μ) (hk : MeasureTheory.AEStronglyMeasurable k μ) (hfg : ∀ᵐ (y : G) ∂μ, ConvolutionExistsAt f g y L) (hgk : ∀ᵐ (x : G) ∂ν, ConvolutionExistsAt (fun (x : G) => ‖g x‖) (fun (x : G) => ‖k x‖) x (ContinuousLinearMap.mul ℝ ℝ)) (hfgk : ConvolutionExistsAt (fun (x : G) => ‖f x‖) (convolution (fun (x : G) => ‖g x‖) (fun (x : G) => ‖k x‖) (ContinuousLinearMap.mul ℝ ℝ)) x₀ (ContinuousLinearMap.mul ℝ ℝ)) : convolution (convolution f g L) k L₂ x₀ = convolution f (convolution g k L₄) L₃ x₀

Convolution is associative. This requires that

• all maps are a.e. strongly measurable w.r.t one of the measures
• f ⋆[L, ν] g exists almost everywhere
• ‖g‖ ⋆[μ] ‖k‖ exists almost everywhere
• ‖f‖ ⋆[ν] (‖g‖ ⋆[μ] ‖k‖) exists at x₀

theorem convolution_precompR_apply {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {E'' : Type uE''} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup E''] [NormedAddCommGroup F] {f : G → E} [IsROrC 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 E''] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [CompleteSpace F] [MeasurableSpace G] {μ : MeasureTheory.Measure G} (L : E →L[𝕜] E' →L[𝕜] F) [NormedAddCommGroup G] [BorelSpace G] {g : G → E'' →L[𝕜] E'} (hf : MeasureTheory.LocallyIntegrable f) (hcg : HasCompactSupport g) (hg : Continuous g) (x₀ : G) (x : E'') : (convolution f g (ContinuousLinearMap.precompR E'' L) x₀) x = convolution f (fun (a : G) => (g a) x) L x₀

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'} [IsROrC 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [CompleteSpace F] [MeasurableSpace G] {μ : MeasureTheory.Measure G} (L : E →L[𝕜] E' →L[𝕜] F) [NormedAddCommGroup G] [BorelSpace G] [NormedSpace 𝕜 G] [MeasureTheory.SigmaFinite μ] [MeasureTheory.Measure.IsAddLeftInvariant μ] (hcg : HasCompactSupport g) (hf : MeasureTheory.LocallyIntegrable f) (hg : ContDiff 𝕜 1 g) (x₀ : G) : HasFDerivAt (convolution f g L) (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'} [IsROrC 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [CompleteSpace F] [MeasurableSpace G] {μ : MeasureTheory.Measure G} (L : E →L[𝕜] E' →L[𝕜] F) [NormedAddCommGroup G] [BorelSpace G] [NormedSpace 𝕜 G] [MeasureTheory.SigmaFinite μ] [MeasureTheory.Measure.IsAddLeftInvariant μ] [MeasureTheory.Measure.IsNegInvariant μ] (hcf : HasCompactSupport f) (hf : ContDiff 𝕜 1 f) (hg : MeasureTheory.LocallyIntegrable g) (x₀ : G) : HasFDerivAt (convolution f g L) (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] [IsROrC 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace ℝ F] [NormedSpace 𝕜 F] {f₀ : 𝕜 → E} {g₀ : 𝕜 → E'} (L : E →L[𝕜] E' →L[𝕜] F) [CompleteSpace F] {μ : MeasureTheory.Measure 𝕜} [MeasureTheory.Measure.IsAddLeftInvariant μ] [MeasureTheory.SigmaFinite μ] (hf : MeasureTheory.LocallyIntegrable f₀) (hcg : HasCompactSupport g₀) (hg : ContDiff 𝕜 1 g₀) (x₀ : 𝕜) : HasDerivAt (convolution f₀ g₀ L) (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] [IsROrC 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace ℝ F] [NormedSpace 𝕜 F] {f₀ : 𝕜 → E} {g₀ : 𝕜 → E'} (L : E →L[𝕜] E' →L[𝕜] F) [CompleteSpace F] {μ : MeasureTheory.Measure 𝕜} [MeasureTheory.Measure.IsAddLeftInvariant μ] [MeasureTheory.SigmaFinite μ] [MeasureTheory.Measure.IsNegInvariant μ] (hcf : HasCompactSupport f₀) (hf : ContDiff 𝕜 1 f₀) (hg : MeasureTheory.LocallyIntegrable g₀) (x₀ : 𝕜) : HasDerivAt (convolution f₀ g₀ L) (convolution (deriv f₀) g₀ L x₀) x₀

theorem 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} [IsROrC 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [CompleteSpace F] [MeasurableSpace G] [NormedAddCommGroup G] [BorelSpace G] [NormedSpace 𝕜 G] [NormedAddCommGroup P] [NormedSpace 𝕜 P] {μ : MeasureTheory.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 : MeasureTheory.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 contDiffOn_convolution_right_with_param_aux {𝕜 : Type u𝕜} {E : Type uE} [NormedAddCommGroup E] [IsROrC 𝕜] [NormedSpace 𝕜 E] {G : Type uP} {E' : Type uP} {F : Type uP} {P : Type uP} [NormedAddCommGroup E'] [NormedAddCommGroup F] [NormedSpace 𝕜 E'] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [CompleteSpace F] [MeasurableSpace G] {μ : MeasureTheory.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 : MeasureTheory.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 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] [IsROrC 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [CompleteSpace F] [MeasurableSpace G] [NormedAddCommGroup G] [BorelSpace G] [NormedSpace 𝕜 G] [NormedAddCommGroup P] [NormedSpace 𝕜 P] {μ : MeasureTheory.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 : MeasureTheory.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 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] [IsROrC 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [CompleteSpace F] [MeasurableSpace G] [NormedAddCommGroup G] [BorelSpace G] [NormedSpace 𝕜 G] [NormedAddCommGroup P] [NormedSpace 𝕜 P] {μ : MeasureTheory.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 : MeasureTheory.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 smooth function.

theorem 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] [IsROrC 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [CompleteSpace F] [MeasurableSpace G] [NormedAddCommGroup G] [BorelSpace G] [NormedSpace 𝕜 G] [NormedAddCommGroup P] [NormedSpace 𝕜 P] {μ : MeasureTheory.Measure G} [MeasureTheory.Measure.IsAddLeftInvariant μ] [MeasureTheory.Measure.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 : MeasureTheory.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 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] [IsROrC 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [CompleteSpace F] [MeasurableSpace G] [NormedAddCommGroup G] [BorelSpace G] [NormedSpace 𝕜 G] [NormedAddCommGroup P] [NormedSpace 𝕜 P] {μ : MeasureTheory.Measure G} [MeasureTheory.Measure.IsAddLeftInvariant μ] [MeasureTheory.Measure.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 : MeasureTheory.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 smooth 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'} [IsROrC 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [CompleteSpace 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 (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'} [IsROrC 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [CompleteSpace F] [MeasurableSpace G] [NormedAddCommGroup G] [BorelSpace G] [NormedSpace 𝕜 G] {μ : MeasureTheory.Measure G} (L : E →L[𝕜] E' →L[𝕜] F) [MeasureTheory.Measure.IsAddLeftInvariant μ] [MeasureTheory.Measure.IsNegInvariant μ] {n : ℕ∞} (hcf : HasCompactSupport f) (hf : ContDiff 𝕜 n f) (hg : MeasureTheory.LocallyIntegrable g) : ContDiff 𝕜 n (convolution f g L)

noncomputable def posConvolution {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ E'] [NormedSpace ℝ F] (f : ℝ → E) (g : ℝ → E') (L : E →L[ℝ] E' →L[ℝ] F) (ν : autoParam (MeasureTheory.Measure ℝ) _auto✝) : ℝ → F

The forward convolution of two functions f and g on ℝ, with respect to a continuous bilinear map L and measure ν. It is defined to be the function mapping x to ∫ t in 0..x, L (f t) (g (x - t)) ∂ν if 0 < x, and 0 otherwise.

Equations

• posConvolution f g L = Set.indicator (Set.Ioi 0) fun (x : ℝ) => ∫ (t : ℝ) in 0 ..x, (L (f t)) (g (x - t)) ∂ν

theorem posConvolution_eq_convolution_indicator {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ E'] [NormedSpace ℝ F] (f : ℝ → E) (g : ℝ → E') (L : E →L[ℝ] E' →L[ℝ] F) (ν : autoParam (MeasureTheory.Measure ℝ) _auto✝) [MeasureTheory.NoAtoms ν] : posConvolution f g L = convolution (Set.indicator (Set.Ioi 0) f) (Set.indicator (Set.Ioi 0) g) L

theorem integrable_posConvolution {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ E'] [NormedSpace ℝ F] {f : ℝ → E} {g : ℝ → E'} {μ : MeasureTheory.Measure ℝ} {ν : MeasureTheory.Measure ℝ} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] [MeasureTheory.Measure.IsAddRightInvariant μ] [MeasureTheory.NoAtoms ν] (hf : MeasureTheory.IntegrableOn f (Set.Ioi 0)) (hg : MeasureTheory.IntegrableOn g (Set.Ioi 0)) (L : E →L[ℝ] E' →L[ℝ] F) : MeasureTheory.Integrable (posConvolution f g L)

theorem integral_posConvolution {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ E'] [NormedSpace ℝ F] [CompleteSpace F] [CompleteSpace E] [CompleteSpace E'] {μ : MeasureTheory.Measure ℝ} {ν : MeasureTheory.Measure ℝ} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] [MeasureTheory.Measure.IsAddRightInvariant μ] [MeasureTheory.NoAtoms ν] {f : ℝ → E} {g : ℝ → E'} (hf : MeasureTheory.IntegrableOn f (Set.Ioi 0)) (hg : MeasureTheory.IntegrableOn g (Set.Ioi 0)) (L : E →L[ℝ] E' →L[ℝ] F) : ∫ (x : ℝ) in Set.Ioi 0, ∫ (t : ℝ) in 0 ..x, (L (f t)) (g (x - t)) ∂ν ∂μ = (L (∫ (x : ℝ) in Set.Ioi 0, f x ∂ν)) (∫ (x : ℝ) in Set.Ioi 0, g x ∂μ)

The integral over Ioi 0 of a forward convolution of two functions is equal to the product of their integrals over this set. (Compare integral_convolution for the two-sided convolution.)