Smoothness of convolutions with dominated kernels

Mathlib differentiates a convolution f ⋆ g under the integral sign when one factor is C^n with compact support (HasCompactSupport.contDiff_convolution_right). Kernels such as the heat kernel are not compactly supported, but their derivatives decay fast enough to be dominated, uniformly over unit translates, by integrable functions: for each order n there is an integrable φ with ‖D^n g (z + h)‖ ≤ φ z whenever ‖h‖ ≤ 1. This file proves that if the other factor is essentially bounded, then f ⋆ g is as smooth as g, and its derivatives are computed by differentiating g under the integral. The first-order argument is that of Mathlib's HasCompactSupport.hasFDerivAt_convolution_right, with the compact-support bound replaced by the domination hypothesis.

The dominated results use a measure invariant under translations and negation. Translations, negation and open sets are measurable. The continuity theorem needs a seminormed abelian domain, any nontrivially normed scalar field, and second-countability of either the domain or the kernel's codomain. The convolution codomain also carries the real normed-space structure needed for the Bochner integral. The dominated derivative statements use a second-countable real normed domain.

The iterated derivative of f ⋆[L, μ] g is a convolution against the iterated derivative of g, for the bilinear map L_n sending (a, B) to the multilinear map m ↦ L a (B m) (ContinuousLinearMap.compContinuousMultilinearMapL composed with L).

For a compactly supported C^N factor, HasCompactSupport.iteratedFDeriv_convolution_right computes the n-th derivative for n ≤ N on that factor, without a domination assumption.

For a compactly supported C¹ factor g, the file also records the directional form ∂ᵥ (f ⋆ g) = f ⋆ ∂ᵥ g of Mathlib's rule HasCompactSupport.hasFDerivAt_convolution_right, in which the derivative is a convolution with values in F rather than in a space of linear maps.

For mollification by a nonnegative compactly supported kernel ρ of integral 1, the file records two bounds that need no regularity of the mollified function u. One-sided bounds on the forward differences of u in a direction pass to the directional derivative of ρ ⋆ u: this is how a nonsmooth subsolution of a Hamilton–Jacobi inequality, such as a Hopf–Lax function, becomes a smooth one. And a bounded u has a mollification with bounded derivative, hence Lipschitz.

Main declarations

• MeasureTheory.continuous_convolution_right_of_dominated: continuity of f ⋆ g.
• MeasureTheory.hasFDerivAt_convolution_right_of_dominated: D (f ⋆ g) = f ⋆ D g.
• MeasureTheory.iteratedFDeriv_convolution_right_of_dominated: D^n (f ⋆ g) = f ⋆ D^n g.
• MeasureTheory.contDiff_convolution_right_of_dominated, MeasureTheory.contDiff_convolution_left_of_dominated: f ⋆ g is C^N when the smooth factor is.
• MeasureTheory.iteratedFDeriv_convolution_left_of_dominated: D^n (f ⋆ g) = D^n f ⋆ g.
• HasCompactSupport.iteratedFDeriv_convolution_right: D^n (f ⋆ g) = f ⋆ D^n g for compactly supported C^N g and n ≤ N.
• HasCompactSupport.fderiv_convolution_right_apply: for g compactly supported, the directional derivative ∂ᵥ (f ⋆ g) = f ⋆ ∂ᵥ g.
• HasCompactSupport.fderiv_fderiv_convolution_right_apply: the same for two directional derivatives, ∂ᵥ ∂ᵥ' (f ⋆ g) = f ⋆ ∂ᵥ ∂ᵥ' g.
• HasCompactSupport.fderiv_convolution_left_apply_le: mollifying by a nonnegative kernel of integral 1 turns a one-sided bound u (y + s • d) ≤ u y + s * c on forward differences into the bound ∂_d (ρ ⋆ u) ≤ c on the directional derivative.
• HasCompactSupport.norm_fderiv_convolution_left_le: the mollification of a function bounded by M has derivative bounded by M * ∫ ‖Dρ‖.
• HasCompactSupport.lipschitzWith_convolution_left: so it is Lipschitz with constant M * ∫ ‖Dρ‖.

theorem MeasureTheory.continuous_convolution_right_of_dominated {G : Type u_1} {E : Type u_2} {E' : Type u_3} {F : Type u_4} {f : G → E} {g : G → E'} {φ : G → ℝ} {M : ℝ} {𝕜 : Type u_5} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ F] [MeasurableSpace G] {μ : Measure G} [SeminormedAddCommGroup G] [OpensMeasurableSpace G] [MeasurableAdd G] [MeasurableNeg G] [SecondCountableTopologyEither G E'] [μ.IsAddLeftInvariant] [μ.IsNegInvariant] (L : E →L[𝕜] E' →L[𝕜] F) (hf : AEStronglyMeasurable f μ) (hfM : ∀ᵐ (t : G) ∂μ, ‖f t‖ ≤ M) (hg : Continuous g) (hφ : Integrable φ μ) (hgφ : ∀ (z h : G), ‖h‖ ≤ 1 → ‖g (z + h)‖ ≤ φ z) : Continuous (convolution f g L μ)

The convolution of an essentially bounded function with a continuous function that is dominated, uniformly on unit translates, by an integrable function is continuous.

theorem HasCompactSupport.iteratedFDeriv_convolution_right {G : Type u_1} {E : Type u_2} {E' : Type u_3} {F : Type u_4} {f : G → E} {g : G → E'} {𝕜 : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [MeasurableSpace G] {μ : MeasureTheory.Measure G} {N : ℕ∞} (L : E →L[𝕜] E' →L[𝕜] F) [NormedAddCommGroup G] [NormedSpace 𝕜 G] [BorelSpace G] [MeasureTheory.SFinite μ] [μ.IsAddLeftInvariant] (hcg : HasCompactSupport g) (hf : MeasureTheory.LocallyIntegrable f μ) (hg : ContDiff 𝕜 (↑N) g) {n : ℕ} (hn : ↑n ≤ N) : iteratedFDeriv 𝕜 n (MeasureTheory.convolution f g L μ) = MeasureTheory.convolution f (iteratedFDeriv 𝕜 n g) (ContinuousLinearMap.compContinuousMultilinearMapL 𝕜 (fun (x : Fin n) => G) E' F ∘SL L) μ

For a compactly supported C^N factor g, the n-th convolution derivative for n ≤ N is computed on g. The other factor need only be locally integrable.

theorem MeasureTheory.hasFDerivAt_convolution_right_of_dominated {G : Type u_1} {E : Type u_2} {E' : Type u_3} {F : Type u_4} {f : G → E} {g : G → E'} {φ : G → ℝ} {M : ℝ} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace G] {μ : Measure G} (L : E →L[ℝ] E' →L[ℝ] F) [NormedAddCommGroup G] [NormedSpace ℝ G] [OpensMeasurableSpace G] [MeasurableAdd G] [MeasurableNeg G] [SecondCountableTopology G] [μ.IsAddLeftInvariant] [μ.IsNegInvariant] (hf : AEStronglyMeasurable f μ) (hfM : ∀ᵐ (t : G) ∂μ, ‖f t‖ ≤ M) (hg : ContDiff ℝ 1 g) (hgi : Integrable g μ) (hφ : Integrable φ μ) (hgφ : ∀ (z h : G), ‖h‖ ≤ 1 → ‖fderiv ℝ g (z + h)‖ ≤ φ z) (x₀ : G) : HasFDerivAt (convolution f g L μ) (convolution f (fderiv ℝ g) (ContinuousLinearMap.precompR G L) μ x₀) x₀

Differentiating a convolution under the integral. Let f be essentially bounded and g be C¹ and integrable, with D g dominated, uniformly on unit translates, by an integrable function. Then D (f ⋆ g) = f ⋆ D g.

theorem MeasureTheory.iteratedFDeriv_convolution_right_of_dominated {G : Type u_1} {E : Type u_2} {E' : Type u_3} {F : Type u_4} {f : G → E} {g : G → E'} {M : ℝ} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace G] {μ : Measure G} {N : ℕ∞} (L : E →L[ℝ] E' →L[ℝ] F) [NormedAddCommGroup G] [NormedSpace ℝ G] [OpensMeasurableSpace G] [MeasurableAdd G] [MeasurableNeg G] [SecondCountableTopology G] [μ.IsAddLeftInvariant] [μ.IsNegInvariant] (hf : AEStronglyMeasurable f μ) (hfM : ∀ᵐ (t : G) ∂μ, ‖f t‖ ≤ M) (hg : ContDiff ℝ (↑N) g) (hgφ : ∀ (n : ℕ), ↑n ≤ N → ∃ (φ : G → ℝ), Integrable φ μ ∧ ∀ (z h : G), ‖h‖ ≤ 1 → ‖iteratedFDeriv ℝ n g (z + h)‖ ≤ φ z) {n : ℕ} (hn : ↑n ≤ N) : iteratedFDeriv ℝ n (convolution f g L μ) = convolution f (iteratedFDeriv ℝ n g) (ContinuousLinearMap.compContinuousMultilinearMapL ℝ (fun (x : Fin n) => G) E' F ∘SL L) μ

Iterated derivatives of a convolution. Let f be essentially bounded and g be C^N, with each derivative of order at most N dominated, uniformly on unit translates, by an integrable function. Then for n ≤ N, D^n (f ⋆[L] g) = f ⋆[L_n] D^n g, where L_n a B = (m ↦ L a (B m)).

theorem MeasureTheory.contDiff_convolution_right_of_dominated {G : Type u_1} {E : Type u_2} {E' : Type u_3} {F : Type u_4} {f : G → E} {g : G → E'} {M : ℝ} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace G] {μ : Measure G} {N : ℕ∞} (L : E →L[ℝ] E' →L[ℝ] F) [NormedAddCommGroup G] [NormedSpace ℝ G] [OpensMeasurableSpace G] [MeasurableAdd G] [MeasurableNeg G] [SecondCountableTopology G] [μ.IsAddLeftInvariant] [μ.IsNegInvariant] (hf : AEStronglyMeasurable f μ) (hfM : ∀ᵐ (t : G) ∂μ, ‖f t‖ ≤ M) (hg : ContDiff ℝ (↑N) g) (hgφ : ∀ (n : ℕ), ↑n ≤ N → ∃ (φ : G → ℝ), Integrable φ μ ∧ ∀ (z h : G), ‖h‖ ≤ 1 → ‖iteratedFDeriv ℝ n g (z + h)‖ ≤ φ z) : ContDiff ℝ (↑N) (convolution f g L μ)

Smoothness of a convolution. Let f be essentially bounded and g be C^N, with each derivative of order at most N dominated, uniformly on unit translates, by an integrable function. Then f ⋆ g is C^N.

theorem MeasureTheory.contDiff_convolution_left_of_dominated {G : Type u_1} {E : Type u_2} {E' : Type u_3} {F : Type u_4} {f : G → E} {g : G → E'} {M : ℝ} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace G] {μ : Measure G} {N : ℕ∞} (L : E →L[ℝ] E' →L[ℝ] F) [NormedAddCommGroup G] [NormedSpace ℝ G] [OpensMeasurableSpace G] [MeasurableAdd G] [MeasurableNeg G] [SecondCountableTopology G] [μ.IsAddLeftInvariant] [μ.IsNegInvariant] (hf : ContDiff ℝ (↑N) f) (hfφ : ∀ (n : ℕ), ↑n ≤ N → ∃ (φ : G → ℝ), Integrable φ μ ∧ ∀ (z h : G), ‖h‖ ≤ 1 → ‖iteratedFDeriv ℝ n f (z + h)‖ ≤ φ z) (hg : AEStronglyMeasurable g μ) (hgM : ∀ᵐ (t : G) ∂μ, ‖g t‖ ≤ M) : ContDiff ℝ (↑N) (convolution f g L μ)

Smoothness of a convolution, with the smooth factor on the left.

theorem MeasureTheory.iteratedFDeriv_convolution_left_of_dominated {G : Type u_1} {E : Type u_2} {E' : Type u_3} {F : Type u_4} {f : G → E} {g : G → E'} {M : ℝ} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace G] {μ : Measure G} {N : ℕ∞} (L : E →L[ℝ] E' →L[ℝ] F) [NormedAddCommGroup G] [NormedSpace ℝ G] [OpensMeasurableSpace G] [MeasurableAdd G] [MeasurableNeg G] [SecondCountableTopology G] [μ.IsAddLeftInvariant] [μ.IsNegInvariant] (hf : ContDiff ℝ (↑N) f) (hfφ : ∀ (n : ℕ), ↑n ≤ N → ∃ (φ : G → ℝ), Integrable φ μ ∧ ∀ (z h : G), ‖h‖ ≤ 1 → ‖iteratedFDeriv ℝ n f (z + h)‖ ≤ φ z) (hg : AEStronglyMeasurable g μ) (hgM : ∀ᵐ (t : G) ∂μ, ‖g t‖ ≤ M) {n : ℕ} (hn : ↑n ≤ N) : iteratedFDeriv ℝ n (convolution f g L μ) = convolution (iteratedFDeriv ℝ n f) g (ContinuousLinearMap.compContinuousMultilinearMapL ℝ (fun (x : Fin n) => G) E F ∘SL L.flip).flip μ

Iterated derivatives of a convolution, with the smooth factor on the left: D^n (f ⋆[L] g) = D^n f ⋆[L'_n] g, where L'_n A b = (m ↦ L (A m) b).

theorem HasCompactSupport.fderiv_convolution_right_apply {G : Type u_1} {E : Type u_2} {E' : Type u_3} {F : Type u_4} {f : G → E} {g : G → E'} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace G] {μ : MeasureTheory.Measure G} (L : E →L[ℝ] E' →L[ℝ] F) [NormedAddCommGroup G] [NormedSpace ℝ G] [BorelSpace G] [MeasureTheory.SFinite μ] [μ.IsAddLeftInvariant] (hcg : HasCompactSupport g) (hf : MeasureTheory.LocallyIntegrable f μ) (hg : ContDiff ℝ 1 g) (x v : G) : (fderiv ℝ (MeasureTheory.convolution f g L μ) x) v = MeasureTheory.convolution f (fun (y : G) => (fderiv ℝ g y) v) L μ x

Directional derivatives of a convolution. If f is locally integrable and g is C¹ with compact support, then the derivative of f ⋆ g in a direction v is the convolution of f with the derivative of g in the direction v.

theorem HasCompactSupport.fderiv_fderiv_convolution_right_apply {G : Type u_1} {E : Type u_2} {E' : Type u_3} {F : Type u_4} {f : G → E} {g : G → E'} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace G] {μ : MeasureTheory.Measure G} (L : E →L[ℝ] E' →L[ℝ] F) [NormedAddCommGroup G] [NormedSpace ℝ G] [BorelSpace G] [MeasureTheory.SFinite μ] [μ.IsAddLeftInvariant] (hcg : HasCompactSupport g) (hf : MeasureTheory.LocallyIntegrable f μ) (hg : ContDiff ℝ 2 g) (x v w : G) : (fderiv ℝ (fun (y : G) => (fderiv ℝ (MeasureTheory.convolution f g L μ) y) w) x) v = MeasureTheory.convolution f (fun (y : G) => (fderiv ℝ (fun (z : G) => (fderiv ℝ g z) w) y) v) L μ x

Iterated directional derivatives of a convolution fall on the compactly supported factor. If f is locally integrable and g is C² with compact support, then the derivative in the direction v of the derivative of f ⋆ g in the direction w is the convolution of f with the corresponding second derivative of g.

theorem HasCompactSupport.fderiv_convolution_left_apply_le {G : Type u_1} [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedAddCommGroup G] [NormedSpace ℝ G] [BorelSpace G] [MeasureTheory.SFinite μ] [μ.IsAddLeftInvariant] [μ.IsNegInvariant] {ρ : G → ℝ} (hρc : HasCompactSupport ρ) (hρ : ContDiff ℝ 1 ρ) (hρ0 : ∀ (y : G), 0 ≤ ρ y) (hρ1 : ∫ (y : G), ρ y ∂μ = 1) {u : G → ℝ} (hu : MeasureTheory.LocallyIntegrable u μ) {x d : G} {c : ℝ} (h : ∀ᶠ (s : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ z ∈ Function.support ρ, u (x - z + s • d) ≤ u (x - z) + s * c) : (fderiv ℝ (MeasureTheory.convolution ρ u (ContinuousLinearMap.lsmul ℝ ℝ) μ) x) d ≤ c

Mollifying a one-sided difference bound. Let ρ be a nonnegative C¹ compactly supported kernel of integral 1 and u a locally integrable function. If, for all small s > 0, the forward difference u (y + s • d) - u y is at most s * c at every point y = x - z with z in the support of ρ, then the derivative of the mollification ρ ⋆ u at x in the direction d is at most c. No regularity of u is needed.

theorem HasCompactSupport.norm_fderiv_convolution_left_le {G : Type u_1} {E' : Type u_3} {M : ℝ} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedAddCommGroup G] [NormedSpace ℝ G] [BorelSpace G] [μ.IsAddLeftInvariant] [μ.IsNegInvariant] {ρ : G → ℝ} [MeasureTheory.IsFiniteMeasureOnCompacts μ] (hρc : HasCompactSupport ρ) (hρ : ContDiff ℝ 1 ρ) {u : G → E'} (hu : MeasureTheory.LocallyIntegrable u μ) (huM : ∀ (y : G), ‖u y‖ ≤ M) (x : G) : ‖fderiv ℝ (MeasureTheory.convolution ρ u (ContinuousLinearMap.lsmul ℝ ℝ) μ) x‖ ≤ M * ∫ (y : G), ‖fderiv ℝ ρ y‖ ∂μ

The mollification ρ ⋆ u of a function bounded by M, by a C¹ compactly supported kernel ρ, has derivative bounded by M * ∫ ‖Dρ‖, uniformly in the point.

theorem HasCompactSupport.lipschitzWith_convolution_left {G : Type u_1} {E' : Type u_3} {M : ℝ} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedAddCommGroup G] [NormedSpace ℝ G] [BorelSpace G] [μ.IsAddLeftInvariant] [μ.IsNegInvariant] {ρ : G → ℝ} [MeasureTheory.IsFiniteMeasureOnCompacts μ] (hρc : HasCompactSupport ρ) (hρ : ContDiff ℝ 1 ρ) {u : G → E'} (hu : MeasureTheory.LocallyIntegrable u μ) (huM : ∀ (y : G), ‖u y‖ ≤ M) : LipschitzWith (M * ∫ (y : G), ‖fderiv ℝ ρ y‖ ∂μ).toNNReal (MeasureTheory.convolution ρ u (ContinuousLinearMap.lsmul ℝ ℝ) μ)

The mollification ρ ⋆ u of a function bounded by M, by a C¹ compactly supported kernel ρ, is Lipschitz with constant M * ∫ ‖Dρ‖.