Convolution existence and continuous linear maps

An essentially bounded function convolves with an integrable function at every point of a measurable additive group with a measure invariant under left translations and negation (MeasureTheory.convolutionExists_of_ae_norm_le_of_integrable and MeasureTheory.convolutionExists_of_integrable_of_ae_norm_le). No topology on the group or sigma-finiteness of the measure is required. For two integrable scalar kernels and an essentially bounded function, convolution is associative at every point; this associativity statement additionally assumes s-finiteness.

A continuous linear map L : F →L[𝕜] F' between real or complex Banach spaces commutes with convolution against a scalar kernel ρ : G → 𝕜: ρ ⋆ (L ∘ f) = L (ρ ⋆ f) at every point where ρ ⋆ f exists (ContinuousLinearMap.convolution_lsmul_comp_comm). This is the convolution form of ContinuousLinearMap.integral_comp_comm. It lets a mollification be moved through a continuous linear map, for instance to mollify the image of a function in a dual space.

Mollification by a nonnegative real kernel ρ of integral 1 supported in ball 0 R preserves one-sided bounds: a lower (upper) bound on g over ball x₀ R is a lower (upper) bound on (ρ ⋆ g) x₀, and a bound on the norm of a vector-valued f over ball x₀ R bounds the norm of (ρ ⋆ f) x₀. So as the supports of the kernels shrink, the mollifications of a function lower (upper) semicontinuous at x₀ eventually lie almost above (below) its value there, and the minimum (maximum) of the mollification and the function tends to that value.

A convolution (f ⋆ g) x only sees g at the points x - t with t in the support of f, so g may be replaced by its indicator on any set containing them. Consequently, pairing a convolution ρ ⋆ u with a continuous compactly supported ψ only involves u on the compact set tsupport ψ - tsupport ρ, and Fubini moves the kernel outside: ∫ ψ (ρ ⋆ u) = ∫ ρ(t) (∫ ψ(x) u(x - t) dx) dt for u locally integrable near that set.

Against a kernel f of integral zero supported in ball 0 R, the constant g x₀ convolves to zero, so (f ⋆ g) x₀ is bounded by ‖L‖ (∫ ‖f‖) times the oscillation of g on ball x₀ R.

For a continuous compactly supported kernel ψ and a locally integrable f, writing f x - (ψ ⋆ f) x and (ψ ⋆ f) x - (ψ ⋆ f) y as single integrals bounds them by ψ-weighted integrals of increments of f; when ψ has integral 1, is bounded by M and vanishes off closedBall 0 t, the first is at most M times the integral of ‖f x - f w‖ₑ over w ∈ closedBall x t.

Main declarations

• MeasureTheory.convolutionExists_of_ae_norm_le_of_integrable, MeasureTheory.convolutionExists_of_integrable_of_ae_norm_le: existence of f ⋆ g when one factor is integrable and the other essentially bounded.
• MeasureTheory.convolution_eq_zero_of_not_completeSpace: without completeness of the target every convolution is the zero function.
• MeasureTheory.convolution_lsmul_assoc_of_integrable_of_ae_norm_le: pointwise associativity for two integrable kernels and an essentially bounded function.
• ContinuousLinearMap.convolution_lsmul_comp_comm: ρ ⋆ (L ∘ f) = L (ρ ⋆ f).
• MeasureTheory.le_convolution_lsmul_of_forall_le and MeasureTheory.convolution_lsmul_le_of_forall_le: one-sided bounds on a ball pass to the mollification at its centre.
• MeasureTheory.norm_convolution_lsmul_le_of_forall_norm_le: a norm bound on a ball passes to the mollification at its centre.
• MeasureTheory.eventually_lt_convolution_lsmul_of_lowerSemicontinuousAt and MeasureTheory.eventually_convolution_lsmul_lt_of_upperSemicontinuousAt: mollification by shrinking kernels at a point of lower (upper) semicontinuity.
• MeasureTheory.tendsto_min_convolution_lsmul_of_lowerSemicontinuousAt and MeasureTheory.tendsto_max_convolution_lsmul_of_upperSemicontinuousAt: the minimum (maximum) of the mollification and the function converges to the value at a point of lower (upper) semicontinuity.
• MeasureTheory.convolution_indicator_eq_of_forall_sub_mem: replacing g by its indicator on a set containing x - support f does not change (f ⋆ g) x.
• MeasureTheory.integral_mul_convolution_eq_integral_mul_integral_comp_sub: the Fubini identity ∫ ψ (ρ ⋆ u) = ∫ ρ(t) (∫ ψ(x) u(x - t) dx) dt for compactly supported ψ and ρ.
• MeasureTheory.norm_convolution_le_of_integral_eq_zero: convolution with a kernel of integral zero is bounded by the oscillation of the other factor.
• MeasureTheory.enorm_sub_convolution_lsmul_le and MeasureTheory.enorm_sub_convolution_lsmul_le_mul_lintegral: the distance from f x to (ψ ⋆ f) x is bounded by a ψ-weighted integral of the increments ‖f x - f w‖ₑ.
• MeasureTheory.enorm_convolution_lsmul_sub_convolution_lsmul_le: the increments of ψ ⋆ f are bounded by a ψ-weighted integral of the increments of the translates of f.

theorem MeasureTheory.convolution_eq_zero_of_not_completeSpace {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} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [Sub G] [MeasurableSpace G] {μ : Measure G} {L : E →L[𝕜] E' →L[𝕜] F} (hF : ¬CompleteSpace F) : convolution f g L μ = 0

Without completeness of the target F, every Bochner integral valued in F is 0, so every convolution valued in F is the zero function.

theorem MeasureTheory.convolutionExists_of_ae_norm_le_of_integrable {G : Type u_1} {E : Type u_2} {E' : Type u_3} {F : Type u_4} {f : G → E} {g : G → E'} {M : ℝ} {𝕜 : Type u_5} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [AddGroup G] [MeasurableSpace G] [MeasurableAdd G] [MeasurableNeg G] {μ : Measure G} [μ.IsAddLeftInvariant] [μ.IsNegInvariant] (L : E →L[𝕜] E' →L[𝕜] F) (hf : AEStronglyMeasurable f μ) (hfM : ∀ᵐ (t : G) ∂μ, ‖f t‖ ≤ M) (hg : Integrable g μ) : ConvolutionExists f g L μ

An essentially bounded function convolves with an integrable function at every point.

theorem MeasureTheory.convolutionExists_of_integrable_of_ae_norm_le {G : Type u_1} {E : Type u_2} {E' : Type u_3} {F : Type u_4} {f : G → E} {g : G → E'} {M : ℝ} {𝕜 : Type u_5} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [AddGroup G] [MeasurableSpace G] [MeasurableAdd G] [MeasurableNeg G] {μ : Measure G} [μ.IsAddLeftInvariant] [μ.IsNegInvariant] (L : E →L[𝕜] E' →L[𝕜] F) (hf : Integrable f μ) (hg : AEStronglyMeasurable g μ) (hgM : ∀ᵐ (t : G) ∂μ, ‖g t‖ ≤ M) : ConvolutionExists f g L μ

An integrable function convolves with an essentially bounded function at every point.

theorem MeasureTheory.convolution_lsmul_assoc_of_integrable_of_ae_norm_le {𝕜 : Type u_6} {G : Type u_7} {F : Type u_8} [RCLike 𝕜] [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] [MeasurableNeg G] {μ : Measure G} [SFinite μ] [μ.IsAddLeftInvariant] [μ.IsNegInvariant] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [CompleteSpace F] {f g : G → 𝕜} {h : G → F} {M : ℝ} (hf : Integrable f μ) (hg : Integrable g μ) (hh : AEStronglyMeasurable h μ) (hM : ∀ᵐ (x : G) ∂μ, ‖h x‖ ≤ M) : convolution (convolution f g (ContinuousLinearMap.lsmul 𝕜 𝕜) μ) h (ContinuousLinearMap.lsmul 𝕜 𝕜) μ = convolution f (convolution g h (ContinuousLinearMap.lsmul 𝕜 𝕜) μ) (ContinuousLinearMap.lsmul 𝕜 𝕜) μ

Convolution of two integrable scalar kernels with an essentially bounded function is associative at every point, not just almost everywhere.

theorem ContinuousLinearMap.convolution_lsmul_comp_comm {𝕜 : Type u_1} {G : Type u_2} {F : Type u_3} {F' : Type u_4} [RCLike 𝕜] [Sub G] [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ F] [CompleteSpace F] [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] [NormedSpace ℝ F'] [CompleteSpace F'] (L : F →L[𝕜] F') {ρ : G → 𝕜} {f : G → F} {x : G} (h : MeasureTheory.ConvolutionExistsAt ρ f x (lsmul 𝕜 𝕜) μ) : MeasureTheory.convolution ρ (fun (y : G) => L (f y)) (lsmul 𝕜 𝕜) μ x = L (MeasureTheory.convolution ρ f (lsmul 𝕜 𝕜) μ x)

A continuous linear map commutes with convolution against a scalar kernel, at every point where the convolution exists.

theorem MeasureTheory.le_convolution_lsmul_of_forall_le {G : Type u_1} [SeminormedAddCommGroup G] [MeasurableSpace G] {μ : Measure G} {ρ g : G → ℝ} {x₀ : G} {R c : ℝ} (hρs : Function.support ρ ⊆ Metric.ball 0 R) (hρ0 : ∀ (y : G), 0 ≤ ρ y) (hρ1 : ∫ (y : G), ρ y ∂μ = 1) (hg : ConvolutionExistsAt ρ g x₀ (ContinuousLinearMap.lsmul ℝ ℝ) μ) (h : ∀ y ∈ Metric.ball x₀ R, c ≤ g y) : c ≤ convolution ρ g (ContinuousLinearMap.lsmul ℝ ℝ) μ x₀

Lower bounds survive mollification. If ρ is a nonnegative kernel of integral 1 supported in ball 0 R and c ≤ g on ball x₀ R, then c ≤ (ρ ⋆ g) x₀.

theorem MeasureTheory.convolution_lsmul_le_of_forall_le {G : Type u_1} [SeminormedAddCommGroup G] [MeasurableSpace G] {μ : Measure G} {ρ g : G → ℝ} {x₀ : G} {R c : ℝ} (hρs : Function.support ρ ⊆ Metric.ball 0 R) (hρ0 : ∀ (y : G), 0 ≤ ρ y) (hρ1 : ∫ (y : G), ρ y ∂μ = 1) (hg : ConvolutionExistsAt ρ g x₀ (ContinuousLinearMap.lsmul ℝ ℝ) μ) (h : ∀ y ∈ Metric.ball x₀ R, g y ≤ c) : convolution ρ g (ContinuousLinearMap.lsmul ℝ ℝ) μ x₀ ≤ c

Upper bounds survive mollification. If ρ is a nonnegative kernel of integral 1 supported in ball 0 R and g ≤ c on ball x₀ R, then (ρ ⋆ g) x₀ ≤ c.

theorem MeasureTheory.norm_convolution_lsmul_le_of_forall_norm_le {G : Type u_1} [SeminormedAddCommGroup G] [MeasurableSpace G] {μ : Measure G} {ρ : G → ℝ} {x₀ : G} {R : ℝ} {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {f : G → E'} {M : ℝ} (hρs : Function.support ρ ⊆ Metric.ball 0 R) (hρ0 : ∀ (y : G), 0 ≤ ρ y) (hρ1 : ∫ (y : G), ρ y ∂μ = 1) (h : ∀ y ∈ Metric.ball x₀ R, ‖f y‖ ≤ M) : ‖convolution ρ f (ContinuousLinearMap.lsmul ℝ ℝ) μ x₀‖ ≤ M

Sup-norm bounds survive mollification. If ρ is a nonnegative kernel of integral 1 supported in ball 0 R and ‖f‖ ≤ M on ball x₀ R, then ‖(ρ ⋆ f) x₀‖ ≤ M.

theorem MeasureTheory.eventually_lt_convolution_lsmul_of_lowerSemicontinuousAt {G : Type u_1} [SeminormedAddCommGroup G] [MeasurableSpace G] {μ : Measure G} {g : G → ℝ} {x₀ : G} {c : ℝ} {ι : Type u_2} {l : Filter ι} {ρ : ι → G → ℝ} (hρ0 : ∀ᶠ (i : ι) in l, ∀ (y : G), 0 ≤ ρ i y) (hρ1 : ∀ᶠ (i : ι) in l, ∫ (y : G), ρ i y ∂μ = 1) (hρs : Filter.Tendsto (fun (i : ι) => Function.support (ρ i)) l (nhds 0).smallSets) (hg : ∀ᶠ (i : ι) in l, ConvolutionExistsAt (ρ i) g x₀ (ContinuousLinearMap.lsmul ℝ ℝ) μ) (hgx : LowerSemicontinuousAt g x₀) (hc : c < g x₀) : ∀ᶠ (i : ι) in l, c < convolution (ρ i) g (ContinuousLinearMap.lsmul ℝ ℝ) μ x₀

Mollification and lower semicontinuity. Let ρ i be nonnegative kernels of integral 1 whose supports shrink to 0. If g is lower semicontinuous at x₀, then every c < g x₀ is eventually below (ρ i ⋆ g) x₀.

theorem MeasureTheory.eventually_convolution_lsmul_lt_of_upperSemicontinuousAt {G : Type u_1} [SeminormedAddCommGroup G] [MeasurableSpace G] {μ : Measure G} {g : G → ℝ} {x₀ : G} {c : ℝ} {ι : Type u_2} {l : Filter ι} {ρ : ι → G → ℝ} (hρ0 : ∀ᶠ (i : ι) in l, ∀ (y : G), 0 ≤ ρ i y) (hρ1 : ∀ᶠ (i : ι) in l, ∫ (y : G), ρ i y ∂μ = 1) (hρs : Filter.Tendsto (fun (i : ι) => Function.support (ρ i)) l (nhds 0).smallSets) (hg : ∀ᶠ (i : ι) in l, ConvolutionExistsAt (ρ i) g x₀ (ContinuousLinearMap.lsmul ℝ ℝ) μ) (hgx : UpperSemicontinuousAt g x₀) (hc : g x₀ < c) : ∀ᶠ (i : ι) in l, convolution (ρ i) g (ContinuousLinearMap.lsmul ℝ ℝ) μ x₀ < c

Mollification and upper semicontinuity. Let ρ i be nonnegative kernels of integral 1 whose supports shrink to 0. If g is upper semicontinuous at x₀, then every c > g x₀ is eventually above (ρ i ⋆ g) x₀.

theorem MeasureTheory.tendsto_min_convolution_lsmul_of_lowerSemicontinuousAt {G : Type u_1} [SeminormedAddCommGroup G] [MeasurableSpace G] {μ : Measure G} {g : G → ℝ} {x₀ : G} {ι : Type u_2} {l : Filter ι} {ρ : ι → G → ℝ} (hρ0 : ∀ᶠ (i : ι) in l, ∀ (y : G), 0 ≤ ρ i y) (hρ1 : ∀ᶠ (i : ι) in l, ∫ (y : G), ρ i y ∂μ = 1) (hρs : Filter.Tendsto (fun (i : ι) => Function.support (ρ i)) l (nhds 0).smallSets) (hg : ∀ᶠ (i : ι) in l, ConvolutionExistsAt (ρ i) g x₀ (ContinuousLinearMap.lsmul ℝ ℝ) μ) (hgx : LowerSemicontinuousAt g x₀) : Filter.Tendsto (fun (i : ι) => min (convolution (ρ i) g (ContinuousLinearMap.lsmul ℝ ℝ) μ x₀) (g x₀)) l (nhds (g x₀))

Mollification and lower semicontinuity, in the limit. Let ρ i be nonnegative kernels of integral 1 whose supports shrink to 0. If g is lower semicontinuous at x₀, then min ((ρ i ⋆ g) x₀) (g x₀) tends to g x₀.

theorem MeasureTheory.tendsto_max_convolution_lsmul_of_upperSemicontinuousAt {G : Type u_1} [SeminormedAddCommGroup G] [MeasurableSpace G] {μ : Measure G} {g : G → ℝ} {x₀ : G} {ι : Type u_2} {l : Filter ι} {ρ : ι → G → ℝ} (hρ0 : ∀ᶠ (i : ι) in l, ∀ (y : G), 0 ≤ ρ i y) (hρ1 : ∀ᶠ (i : ι) in l, ∫ (y : G), ρ i y ∂μ = 1) (hρs : Filter.Tendsto (fun (i : ι) => Function.support (ρ i)) l (nhds 0).smallSets) (hg : ∀ᶠ (i : ι) in l, ConvolutionExistsAt (ρ i) g x₀ (ContinuousLinearMap.lsmul ℝ ℝ) μ) (hgx : UpperSemicontinuousAt g x₀) : Filter.Tendsto (fun (i : ι) => max (convolution (ρ i) g (ContinuousLinearMap.lsmul ℝ ℝ) μ x₀) (g x₀)) l (nhds (g x₀))

Mollification and upper semicontinuity, in the limit. Let ρ i be nonnegative kernels of integral 1 whose supports shrink to 0. If g is upper semicontinuous at x₀, then max ((ρ i ⋆ g) x₀) (g x₀) tends to g x₀.

theorem MeasureTheory.convolution_indicator_eq_of_forall_sub_mem {𝕜 : Type u_1} {G : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ F] [Sub G] [MeasurableSpace G] {μ : Measure G} (L : E →L[𝕜] E' →L[𝕜] F) {f : G → E} {g : G → E'} {s : Set G} {x : G} (h : ∀ t ∈ Function.support f, x - t ∈ s) : convolution f (s.indicator g) L μ x = convolution f g L μ x

A convolution at x sees g only at the points x - t with t in the support of the kernel f, so g may be replaced by its indicator on any set containing all of them.

theorem MeasureTheory.integral_mul_convolution_eq_integral_mul_integral_comp_sub {G : Type u_1} [NormedAddCommGroup G] [MeasurableSpace G] [BorelSpace G] [SecondCountableTopology G] {μ : Measure G} [SFinite μ] [μ.IsAddRightInvariant] {ψ ρ u : G → ℝ} {s : Set G} (hψ : Continuous ψ) (hψc : HasCompactSupport ψ) (hρ : Integrable ρ μ) (hρc : HasCompactSupport ρ) (hu : LocallyIntegrableOn u s μ) (hs : ∀ t ∈ tsupport ρ, ∀ x ∈ tsupport ψ, x - t ∈ s) : ∫ (x : G), ψ x * convolution ρ u (ContinuousLinearMap.lsmul ℝ ℝ) μ x ∂μ = ∫ (t : G), ρ t * ∫ (x : G), ψ x * u (x - t) ∂μ ∂μ

Pairing a convolution with a test function. For a continuous compactly supported ψ, an integrable compactly supported kernel ρ and a function u locally integrable on a set s containing tsupport ψ - tsupport ρ, Fubini gives ∫ ψ (ρ ⋆ u) = ∫ ρ(t) (∫ ψ(x) u(x - t) dx) dt.

theorem MeasureTheory.norm_convolution_le_of_integral_eq_zero {𝕜 : Type u_1} {G : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ F] [SeminormedAddCommGroup G] [MeasurableSpace G] [BorelSpace G] [SecondCountableTopology G] {μ : Measure G} [μ.IsAddLeftInvariant] [SFinite μ] (L : E →L[𝕜] E' →L[𝕜] F) {f : G → E} {g : G → E'} {x₀ : G} {R w : ℝ} (hw : 0 ≤ w) (hif : Integrable f μ) (hf0 : ∫ (t : G), f t ∂μ = 0) (hf : Function.support f ⊆ Metric.ball 0 R) (hmg : AEStronglyMeasurable g μ) (hg : ∀ x ∈ Metric.ball x₀ R, dist (g x) (g x₀) ≤ w) : ‖convolution f g L μ x₀‖ ≤ (‖L‖ * ∫ (t : G), ‖f t‖ ∂μ) * w

Convolution with a kernel of integral zero. If f is integrable with ∫ f = 0 and supported in ball 0 R, and g stays within w of g x₀ on ball x₀ R, then ‖(f ⋆ g) x₀‖ ≤ ‖L‖ (∫ ‖f‖) w. Only the oscillation of g near x₀ enters, not its size: applied to the derivatives of a mollifier, this bounds the derivatives of a mollification by the local oscillation of the mollified function.

theorem MeasureTheory.enorm_sub_convolution_lsmul_le {G : Type u_1} {F : Type u_2} [NormedAddCommGroup G] [MeasurableSpace G] [BorelSpace G] {μ : Measure G} [μ.IsAddLeftInvariant] [μ.IsNegInvariant] [NormedAddCommGroup F] [NormedSpace ℝ F] {ψ : G → ℝ} {f : G → F} [CompleteSpace F] (hψ : Continuous ψ) (hψc : HasCompactSupport ψ) (hψ1 : ∫ (x : G), ψ x ∂μ = 1) (hf : LocallyIntegrable f μ) (x : G) : ‖f x - convolution ψ f (ContinuousLinearMap.lsmul ℝ ℝ) μ x‖ₑ ≤ ∫⁻ (w : G), ‖ψ (x - w)‖ₑ * ‖f x - f w‖ₑ ∂μ

Mollification moves a function by a weighted average of its increments. If ψ is a continuous compactly supported kernel of integral 1 and f is locally integrable, then ‖f x - (ψ ⋆ f) x‖ₑ is at most the ‖ψ (x - ·)‖ₑ-weighted integral of ‖f x - f w‖ₑ.

theorem MeasureTheory.enorm_convolution_lsmul_sub_convolution_lsmul_le {G : Type u_1} {F : Type u_2} [NormedAddCommGroup G] [MeasurableSpace G] [BorelSpace G] {μ : Measure G} [μ.IsAddLeftInvariant] [μ.IsNegInvariant] [NormedAddCommGroup F] [NormedSpace ℝ F] {ψ : G → ℝ} {f : G → F} (hψ : Continuous ψ) (hψc : HasCompactSupport ψ) (hf : LocallyIntegrable f μ) (x y : G) : ‖convolution ψ f (ContinuousLinearMap.lsmul ℝ ℝ) μ x - convolution ψ f (ContinuousLinearMap.lsmul ℝ ℝ) μ y‖ₑ ≤ ∫⁻ (z : G), ‖ψ z‖ₑ * ‖f (x - z) - f (y - z)‖ₑ ∂μ

Increments of a mollification. For a continuous compactly supported kernel ψ and a locally integrable f, the increments of ψ ⋆ f are bounded by the ‖ψ‖ₑ-weighted integral of the increments of the translates of f.

theorem MeasureTheory.enorm_sub_convolution_lsmul_le_mul_lintegral {G : Type u_1} {F : Type u_2} [NormedAddCommGroup G] [MeasurableSpace G] [BorelSpace G] {μ : Measure G} [μ.IsAddLeftInvariant] [μ.IsNegInvariant] [NormedAddCommGroup F] [NormedSpace ℝ F] {ψ : G → ℝ} {f : G → F} [CompleteSpace F] (hψ : Continuous ψ) (hψc : HasCompactSupport ψ) (hψ1 : ∫ (x : G), ψ x ∂μ = 1) {t : ℝ} (hψt : Function.support ψ ⊆ Metric.closedBall 0 t) {M : ℝ} (hψM : ∀ (x : G), ‖ψ x‖ ≤ M) (hf : LocallyIntegrable f μ) (x : G) : ‖f x - convolution ψ f (ContinuousLinearMap.lsmul ℝ ℝ) μ x‖ₑ ≤ ENNReal.ofReal M * ∫⁻ (w : G) in Metric.closedBall x t, ‖f x - f w‖ₑ ∂μ

Mollification by a bounded kernel of small support. If ψ is a continuous kernel of integral 1 with ‖ψ‖ ≤ M, vanishing off closedBall 0 t, and f is locally integrable, then ‖f x - (ψ ⋆ f) x‖ₑ is at most M times the integral of ‖f x - f w‖ₑ over w ∈ closedBall x t.