Documentation

Mathlib.Analysis.Convolution

Convolution of functions #

This file defines the convolution on two functions, i.e. x ↦ ∫ f(t)g(x - t) ∂t. In the general case, these functions can be vector-valued, and have an arbitrary (additive) group as domain. We use a continuous bilinear operation L on these function values as "multiplication". The domain must be equipped with a Haar measure μ (though many individual results have weaker conditions on μ).

For many applications we can take L = 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

Main Definitions #

Main Results #

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

Notation #

The following notations are localized in the locale convolution:

To do #

theorem MeasureTheory.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 : GE} {g : GE'} [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)) u.indicator (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 : GE} {g : GE'} [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)) u.indicator (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 : GE} {g : GE'} [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)) (-tsupport g + s).indicator (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 : GE} {g : GE'} [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 : GE} {g : GE'} [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) (-tsupport f + s).indicator (fun (t : G) => (L * ⨆ (i : G), f i) * g t) t
def MeasureTheory.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 : GE) (g : GE') (x : G) (L : E →L[𝕜] E' →L[𝕜] F) (μ : autoParam (MeasureTheory.Measure G) _auto✝) :

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
Instances For
    def MeasureTheory.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 : GE) (g : GE') (L : E →L[𝕜] E' →L[𝕜] F) (μ : autoParam (MeasureTheory.Measure G) _auto✝) :

    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
    Instances For
      theorem MeasureTheory.ConvolutionExistsAt.integrable {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : GE} {g : GE'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] {L : E →L[𝕜] E' →L[𝕜] F} [MeasurableSpace G] {μ : MeasureTheory.Measure G} [Sub G] {x : G} (h : MeasureTheory.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 : GE} {g : GE'} [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.SFinite ν] (hf : MeasureTheory.AEStronglyMeasurable f ν) (hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map (fun (p : G × G) => p.1 - p.2) (μ.prod ν))) :
      MeasureTheory.AEStronglyMeasurable (fun (p : G × G) => (L (f p.2)) (g (p.1 - p.2))) (μ.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 : GE} {g : GE'} [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 : GE} {g : GE'} [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 : GE} {g : GE'} [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) (μ.restrict s))) :

      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 MeasureTheory.ConvolutionExistsAt.ofNorm' {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : GE} {g : GE'} [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 : MeasureTheory.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) μ)) :

      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 : GE} {g : GE'} [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.SFinite μ] [μ.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 : GE} {g : GE'} [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.SFinite μ] [μ.IsAddRightInvariant] (hf : MeasureTheory.AEStronglyMeasurable f μ) (hg : MeasureTheory.AEStronglyMeasurable g μ) (x : G) :
      MeasureTheory.AEStronglyMeasurable (fun (t : G) => (L (f (x - t))) (g t)) μ
      theorem MeasureTheory.ConvolutionExistsAt.ofNorm {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : GE} {g : GE'} [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.SFinite μ] [μ.IsAddRightInvariant] {x₀ : G} (h : MeasureTheory.ConvolutionExistsAt (fun (x : G) => f x) (fun (x : G) => g x) x₀ (ContinuousLinearMap.mul ) μ) (hmf : MeasureTheory.AEStronglyMeasurable f μ) (hmg : MeasureTheory.AEStronglyMeasurable g μ) :

      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 : GE} {g : GE'} [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.SFinite μ] [μ.IsAddRightInvariant] [MeasureTheory.SFinite ν] (hf : MeasureTheory.AEStronglyMeasurable f ν) (hg : MeasureTheory.AEStronglyMeasurable g μ) :
      MeasureTheory.AEStronglyMeasurable (fun (p : G × G) => (L (f p.2)) (g (p.1 - p.2))) (μ.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 : GE} {g : GE'} [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.SFinite μ] [μ.IsAddRightInvariant] [MeasureTheory.SFinite ν] (hf : MeasureTheory.Integrable f ν) (hg : MeasureTheory.Integrable g μ) :
      MeasureTheory.Integrable (fun (p : G × G) => (L (f p.2)) (g (p.1 - p.2))) (μ.prod ν)
      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 : GE} {g : GE'} [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.SFinite μ] [μ.IsAddRightInvariant] [MeasureTheory.SFinite ν] (hf : MeasureTheory.Integrable f ν) (hg : MeasureTheory.Integrable g μ) :
      ∀ᵐ (x : G) ∂μ, MeasureTheory.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 : GE} {g : GE'} [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) :
      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 : GE} {g : GE'} [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) :
      theorem BddAbove.convolutionExistsAt {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : GE} {g : GE'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} [AddCommGroup G] [MeasurableNeg G] [μ.IsAddLeftInvariant] [MeasurableAdd₂ G] [MeasureTheory.SFinite μ] {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 μ) :

      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 MeasureTheory.convolutionExistsAt_flip {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : GE} {g : GE'} {x : G} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] {L : E →L[𝕜] E' →L[𝕜] F} [MeasurableSpace G] {μ : MeasureTheory.Measure G} [AddCommGroup G] [MeasurableNeg G] [μ.IsAddLeftInvariant] [MeasurableAdd G] [μ.IsNegInvariant] :
      theorem MeasureTheory.ConvolutionExistsAt.integrable_swap {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : GE} {g : GE'} {x : G} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] {L : E →L[𝕜] E' →L[𝕜] F} [MeasurableSpace G] {μ : MeasureTheory.Measure G} [AddCommGroup G] [MeasurableNeg G] [μ.IsAddLeftInvariant] [MeasurableAdd G] [μ.IsNegInvariant] (h : MeasureTheory.ConvolutionExistsAt f g x L μ) :
      MeasureTheory.Integrable (fun (t : G) => (L (f (x - t))) (g t)) μ
      theorem MeasureTheory.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 : GE} {g : GE'} {x : G} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] {L : E →L[𝕜] E' →L[𝕜] F} [MeasurableSpace G] {μ : MeasureTheory.Measure G} [AddCommGroup G] [MeasurableNeg G] [μ.IsAddLeftInvariant] [MeasurableAdd G] [μ.IsNegInvariant] :
      MeasureTheory.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 : GE} {g : GE'} [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] [μ.IsAddLeftInvariant] [μ.IsNegInvariant] (hcf : HasCompactSupport f) (hf : Continuous f) (hg : MeasureTheory.LocallyIntegrable g μ) :
      theorem HasCompactSupport.convolutionExistsRightOfContinuousLeft {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : GE} {g : GE'} [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] [μ.IsAddLeftInvariant] [μ.IsNegInvariant] (hcg : HasCompactSupport g) (hf : Continuous f) (hg : MeasureTheory.LocallyIntegrable g μ) :
      noncomputable def MeasureTheory.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 : GE) (g : GE') (L : E →L[𝕜] E' →L[𝕜] F) (μ : autoParam (MeasureTheory.Measure G) _auto✝) :
      GF

      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
      Instances For

        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.
        Instances For

          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.
          Instances For

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

            Equations
            Instances For
              theorem MeasureTheory.convolution_def {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : GE} {g : GE'} {x : G} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace F] [Sub G] :
              MeasureTheory.convolution f g L μ x = ∫ (t : G), (L (f t)) (g (x - t))μ
              theorem MeasureTheory.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 : GF} :
              MeasureTheory.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 MeasureTheory.convolution_mul {𝕜 : Type u𝕜} {G : Type uG} {x : G} [NontriviallyNormedField 𝕜] [MeasurableSpace G] {μ : MeasureTheory.Measure G} [Sub G] [NormedSpace 𝕜] {f : G𝕜} {g : G𝕜} :
              MeasureTheory.convolution f g (ContinuousLinearMap.mul 𝕜 𝕜) μ x = ∫ (t : G), f t * g (x - t)μ

              The definition of convolution where the bilinear operator is multiplication.

              theorem MeasureTheory.smul_convolution {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : GE} {g : GE'} [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 : 𝕜} :
              theorem MeasureTheory.convolution_smul {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : GE} {g : GE'} [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 : 𝕜} :
              @[simp]
              theorem MeasureTheory.zero_convolution {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {g : GE'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] {L : E →L[𝕜] E' →L[𝕜] F} [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace F] [AddGroup G] :
              @[simp]
              theorem MeasureTheory.convolution_zero {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : GE} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] {L : E →L[𝕜] E' →L[𝕜] F} [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace F] [AddGroup G] :
              theorem MeasureTheory.ConvolutionExistsAt.distrib_add {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : GE} {g : GE'} {g' : GE'} [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 : MeasureTheory.ConvolutionExistsAt f g x L μ) (hfg' : MeasureTheory.ConvolutionExistsAt f g' x L μ) :
              theorem MeasureTheory.ConvolutionExists.distrib_add {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : GE} {g : GE'} {g' : GE'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] {L : E →L[𝕜] E' →L[𝕜] F} [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace F] [AddGroup G] (hfg : MeasureTheory.ConvolutionExists f g L μ) (hfg' : MeasureTheory.ConvolutionExists f g' L μ) :
              theorem MeasureTheory.ConvolutionExistsAt.add_distrib {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : GE} {f' : GE} {g : GE'} [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 : MeasureTheory.ConvolutionExistsAt f g x L μ) (hfg' : MeasureTheory.ConvolutionExistsAt f' g x L μ) :
              theorem MeasureTheory.ConvolutionExists.add_distrib {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : GE} {f' : GE} {g : GE'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] {L : E →L[𝕜] E' →L[𝕜] F} [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace F] [AddGroup G] (hfg : MeasureTheory.ConvolutionExists f g L μ) (hfg' : MeasureTheory.ConvolutionExists f' g L μ) :
              theorem MeasureTheory.convolution_mono_right_of_nonneg {G : Type uG} {x : G} [MeasurableSpace G] {μ : MeasureTheory.Measure G} [AddGroup G] {f : G} {g : G} {g' : G} (hfg' : MeasureTheory.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) :
              theorem MeasureTheory.convolution_congr {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : GE} {f' : GE} {g : GE'} {g' : GE'} [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.SFinite μ] [μ.IsAddRightInvariant] (h1 : f =ᵐ[μ] f') (h2 : g =ᵐ[μ] g') :
              theorem MeasureTheory.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 : GE} {g : GE'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace F] [AddGroup G] :
              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 : GE} {g : GE'} [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.SFinite μ] [μ.IsAddRightInvariant] (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ) :
              theorem HasCompactSupport.convolution {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : GE} {g : GE'} [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) :
              theorem MeasureTheory.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 : GE} [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 : PGE'} {s : Set P} {k : Set G} (hk : IsCompact k) (hgs : ∀ (p : P) (x : G), p sxkg p x = 0) (hf : MeasureTheory.LocallyIntegrable f μ) (hg : ContinuousOn (g) (s ×ˢ Set.univ)) :
              ContinuousOn (fun (q : P × G) => MeasureTheory.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 MeasureTheory.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 : GE} [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 : PG} (hv : ContinuousOn v s) {g : PGE'} {k : Set G} (hk : IsCompact k) (hgs : ∀ (p : P) (x : G), p sxkg p x = 0) (hf : MeasureTheory.LocallyIntegrable f μ) (hg : ContinuousOn (g) (s ×ˢ Set.univ)) :
              ContinuousOn (fun (x : P) => MeasureTheory.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 : GE} {g : GE'} [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) :

              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 : GE} {g : GE'} [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) :

              The convolution is continuous if one function is integrable and the other is bounded and continuous.

              theorem MeasureTheory.support_convolution_subset {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : GE} {g : GE'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace F] [AddCommGroup G] :
              theorem MeasureTheory.convolution_flip {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : GE} {g : GE'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace F] [AddCommGroup G] [μ.IsAddLeftInvariant] [μ.IsNegInvariant] [MeasurableNeg G] [MeasurableAdd G] :

              Commutativity of convolution

              theorem MeasureTheory.convolution_eq_swap {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : GE} {g : GE'} {x : G} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace F] [AddCommGroup G] [μ.IsAddLeftInvariant] [μ.IsNegInvariant] [MeasurableNeg G] [MeasurableAdd G] :
              MeasureTheory.convolution f g L μ x = ∫ (t : G), (L (f (x - t))) (g t)μ

              The symmetric definition of convolution.

              theorem MeasureTheory.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] [μ.IsAddLeftInvariant] [μ.IsNegInvariant] [MeasurableNeg G] [MeasurableAdd G] {f : G𝕜} {g : GF} :
              MeasureTheory.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 MeasureTheory.convolution_mul_swap {𝕜 : Type u𝕜} {G : Type uG} {x : G} [NontriviallyNormedField 𝕜] [MeasurableSpace G] {μ : MeasureTheory.Measure G} [AddCommGroup G] [μ.IsAddLeftInvariant] [μ.IsNegInvariant] [MeasurableNeg G] [MeasurableAdd G] [NormedSpace 𝕜] {f : G𝕜} {g : G𝕜} :
              MeasureTheory.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 MeasureTheory.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 : GE} {g : GE'} {x : G} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace F] [AddCommGroup G] [μ.IsAddLeftInvariant] [μ.IsNegInvariant] [MeasurableNeg G] [MeasurableAdd G] (h1 : ∀ᵐ (x : G) ∂μ, f (-x) = f x) (h2 : ∀ᵐ (x : G) ∂μ, g (-x) = g 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 : GE} {g : GE'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace F] [AddCommGroup G] [μ.IsAddLeftInvariant] [μ.IsNegInvariant] [TopologicalSpace G] [TopologicalAddGroup G] [BorelSpace G] (hcf : HasCompactSupport f) (hf : Continuous f) (hg : MeasureTheory.LocallyIntegrable g μ) :
              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 : GE} {g : GE'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace F] [AddCommGroup G] [μ.IsAddLeftInvariant] [μ.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 μ) :
              theorem MeasureTheory.convolution_eq_right' {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : GE} {g : GE'} [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 : xMetric.ball x₀ R, g x = g x₀) :
              MeasureTheory.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 MeasureTheory.dist_convolution_le' {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : GE} {g : GE'} [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] [μ.IsAddLeftInvariant] [MeasureTheory.SFinite μ] {x₀ : G} {R : } {ε : } {z₀ : E'} (hε : 0 ε) (hif : MeasureTheory.Integrable f μ) (hf : Function.support f Metric.ball 0 R) (hmg : MeasureTheory.AEStronglyMeasurable g μ) (hg : xMetric.ball x₀ R, dist (g x) z₀ ε) :
              dist (MeasureTheory.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 MeasureTheory.dist_convolution_le {G : Type uG} {E' : Type uE'} [NormedAddCommGroup E'] {g : GE'} [MeasurableSpace G] {μ : MeasureTheory.Measure G} [SeminormedAddCommGroup G] [BorelSpace G] [SecondCountableTopology G] [μ.IsAddLeftInvariant] [MeasureTheory.SFinite μ] [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 : xMetric.ball x₀ R, dist (g x) z₀ ε) :

              Approximate f ⋆ g if the support of the f is bounded within a ball, and g is near g x₀ on a ball with the same radius around x₀.

              This is a special case of dist_convolution_le' where L is (•), f has integral 1 and f is nonnegative.

              theorem MeasureTheory.convolution_tendsto_right {G : Type uG} {E' : Type uE'} [NormedAddCommGroup E'] [MeasurableSpace G] {μ : MeasureTheory.Measure G} [SeminormedAddCommGroup G] [BorelSpace G] [SecondCountableTopology G] [μ.IsAddLeftInvariant] [MeasureTheory.SFinite μ] [NormedSpace E'] [CompleteSpace E'] {ι : Type u_1} {g : ιGE'} {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 (nhds 0).smallSets) (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 : ι) => MeasureTheory.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 MeasureTheory.integral_convolution {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : GE} {g : GE'} [RCLike 𝕜] [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.SFinite μ] [MeasureTheory.SFinite ν] [μ.IsAddRightInvariant] [MeasurableAdd₂ G] [MeasurableNeg G] [NormedSpace E] [NormedSpace E'] [CompleteSpace E] [CompleteSpace E'] (hf : MeasureTheory.Integrable f ν) (hg : MeasureTheory.Integrable g μ) :
              ∫ (x : G), MeasureTheory.convolution f g L ν xμ = (L (∫ (x : G), f xν)) (∫ (x : G), g xμ)
              theorem MeasureTheory.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 : GE} {g : GE'} [RCLike 𝕜] [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 : GE''} (L₂ : F →L[𝕜] E'' →L[𝕜] F') (L₃ : E →L[𝕜] F'' →L[𝕜] F') (L₄ : E' →L[𝕜] E'' →L[𝕜] F'') [AddGroup G] [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] [μ.IsAddRightInvariant] [MeasurableAdd₂ G] [ν.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) ∂μ, MeasureTheory.ConvolutionExistsAt f g y L ν) (hgk : ∀ᵐ (x : G) ∂ν, MeasureTheory.ConvolutionExistsAt g k x L₄ μ) (hi : MeasureTheory.Integrable (Function.uncurry fun (x y : G) => (L₃ (f y)) ((L₄ (g (x - y))) (k (x₀ - x)))) (μ.prod ν)) :

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

              theorem MeasureTheory.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 : GE} {g : GE'} [RCLike 𝕜] [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 : GE''} (L₂ : F →L[𝕜] E'' →L[𝕜] F') (L₃ : E →L[𝕜] F'' →L[𝕜] F') (L₄ : E' →L[𝕜] E'' →L[𝕜] F'') [AddGroup G] [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] [μ.IsAddRightInvariant] [MeasurableAdd₂ G] [ν.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) ∂μ, MeasureTheory.ConvolutionExistsAt f g y L ν) (hgk : ∀ᵐ (x : G) ∂ν, MeasureTheory.ConvolutionExistsAt (fun (x : G) => g x) (fun (x : G) => k x) x (ContinuousLinearMap.mul ) μ) (hfgk : MeasureTheory.ConvolutionExistsAt (fun (x : G) => f x) (MeasureTheory.convolution (fun (x : G) => g x) (fun (x : G) => k x) (ContinuousLinearMap.mul ) μ) x₀ (ContinuousLinearMap.mul ) ν) :

              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 MeasureTheory.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 : GE} [RCLike 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 E''] [NormedSpace F] [NormedSpace 𝕜 F] [MeasurableSpace G] {μ : MeasureTheory.Measure G} (L : E →L[𝕜] E' →L[𝕜] F) [NormedAddCommGroup G] [BorelSpace G] {g : GE'' →L[𝕜] E'} (hf : MeasureTheory.LocallyIntegrable f μ) (hcg : HasCompactSupport g) (hg : Continuous g) (x₀ : G) (x : E'') :
              (MeasureTheory.convolution f g (ContinuousLinearMap.precompR E'' L) μ x₀) x = MeasureTheory.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 : GE} {g : GE'} [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) :

              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 : GE} {g : GE'} [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) :

              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 : GE} [RCLike 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace F] [NormedSpace 𝕜 F] [MeasurableSpace G] [NormedAddCommGroup G] [BorelSpace G] [NormedSpace 𝕜 G] [NormedAddCommGroup P] [NormedSpace 𝕜 P] {μ : MeasureTheory.Measure G} (L : E →L[𝕜] E' →L[𝕜] F) {g : PGE'} {s : Set P} {k : Set G} (hs : IsOpen s) (hk : IsCompact k) (hgs : ∀ (p : P) (x : G), p sxkg 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) => MeasureTheory.convolution f (g q.1) L μ q.2) (MeasureTheory.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 : 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 : GE} {n : ℕ∞} (L : E →L[𝕜] E' →L[𝕜] F) {g : PGE'} {s : Set P} {k : Set G} (hs : IsOpen s) (hk : IsCompact k) (hgs : ∀ (p : P) (x : G), p sxkg p x = 0) (hf : MeasureTheory.LocallyIntegrable f μ) (hg : ContDiffOn 𝕜 n (g) (s ×ˢ Set.univ)) :
              ContDiffOn 𝕜 n (fun (q : P × G) => MeasureTheory.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] [CompleteSpace F] [MeasurableSpace G] [NormedAddCommGroup G] [BorelSpace G] [NormedSpace 𝕜 G] [NormedAddCommGroup P] [NormedSpace 𝕜 P] {μ : MeasureTheory.Measure G} {f : GE} {n : ℕ∞} (L : E →L[𝕜] E' →L[𝕜] F) {g : PGE'} {s : Set P} {k : Set G} (hs : IsOpen s) (hk : IsCompact k) (hgs : ∀ (p : P) (x : G), p sxkg p x = 0) (hf : MeasureTheory.LocallyIntegrable f μ) (hg : ContDiffOn 𝕜 n (g) (s ×ˢ Set.univ)) :
              ContDiffOn 𝕜 n (fun (q : P × G) => MeasureTheory.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] [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 : PG} (hv : ContDiffOn 𝕜 n v s) {f : GE} {g : PGE'} {k : Set G} (hs : IsOpen s) (hk : IsCompact k) (hgs : ∀ (p : P) (x : G), p sxkg p x = 0) (hf : MeasureTheory.LocallyIntegrable f μ) (hg : ContDiffOn 𝕜 n (g) (s ×ˢ Set.univ)) :
              ContDiffOn 𝕜 n (fun (x : P) => MeasureTheory.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 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] [CompleteSpace F] [MeasurableSpace G] [NormedAddCommGroup G] [BorelSpace G] [NormedSpace 𝕜 G] [NormedAddCommGroup P] [NormedSpace 𝕜 P] {μ : MeasureTheory.Measure G} [μ.IsAddLeftInvariant] [μ.IsNegInvariant] (L : E' →L[𝕜] E →L[𝕜] F) {f : GE} {n : ℕ∞} {g : PGE'} {s : Set P} {k : Set G} (hs : IsOpen s) (hk : IsCompact k) (hgs : ∀ (p : P) (x : G), p sxkg p x = 0) (hf : MeasureTheory.LocallyIntegrable f μ) (hg : ContDiffOn 𝕜 n (g) (s ×ˢ Set.univ)) :
              ContDiffOn 𝕜 n (fun (q : P × G) => MeasureTheory.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] [CompleteSpace F] [MeasurableSpace G] [NormedAddCommGroup G] [BorelSpace G] [NormedSpace 𝕜 G] [NormedAddCommGroup P] [NormedSpace 𝕜 P] {μ : MeasureTheory.Measure G} [μ.IsAddLeftInvariant] [μ.IsNegInvariant] (L : E' →L[𝕜] E →L[𝕜] F) {s : Set P} {n : ℕ∞} {v : PG} (hv : ContDiffOn 𝕜 n v s) {f : GE} {g : PGE'} {k : Set G} (hs : IsOpen s) (hk : IsCompact k) (hgs : ∀ (p : P) (x : G), p sxkg p x = 0) (hf : MeasureTheory.LocallyIntegrable f μ) (hg : ContDiffOn 𝕜 n (g) (s ×ˢ Set.univ)) :
              ContDiffOn 𝕜 n (fun (x : P) => MeasureTheory.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 : GE} {g : GE'} [RCLike 𝕜] [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) :
              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 : GE} {g : GE'} [RCLike 𝕜] [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) [μ.IsAddLeftInvariant] [μ.IsNegInvariant] {n : ℕ∞} (hcf : HasCompactSupport f) (hf : ContDiff 𝕜 n f) (hg : MeasureTheory.LocallyIntegrable g μ) :
              noncomputable def MeasureTheory.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
              Instances For
                theorem MeasureTheory.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.SFinite μ] [MeasureTheory.SFinite ν] [μ.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.)