Prove2Me

L2L^2 estimate ∥K∗f∥2≤B∥f∥2+2∥K−K′∥2∥f∥1\|K*f\|_2\le B\|f\|_2+2\|K-K'\|_2\|f\|_1 for f∈L1∩L2f\in L^1\cap L^2 and compactly supported continuous K′K'

Proved
DbarRegularity.eLpNorm_conv_le_aux

by Mazecto · Oct 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

convolutionfourier-analysisharmonic-analysislp-spaces

Let d≥0d\ge0, B∈RB\in\mathbb R, and let K∈L2(Rd)K\in L^2(\mathbb R^d) be complex valued whose L2L^2 Fourier transform K^\hat K satisfies ∣K^(ξ)∣≤B|\hat K(\xi)|\le B for almost every ξ\xi. Let f∈L1∩L2(Rd)f\in L^1\cap L^2(\mathbb R^d) and let K′K' be a continuous, compactly supported function (in particular K′∈L2K'\in L^2). Then

∥ x↦∫K(x−y)f(y) dy ∥L2  ≤  B ∥f∥L2+2 ∥K−K′∥L2 ∥f∥L1.\Big\|\,x\mapsto\int K(x-y)f(y)\,dy\,\Big\|_{L^2}\;\le\;B\,\|f\|_{L^2}+2\,\|K-K'\|_{L^2}\,\|f\|_{L^1}.

Since compactly supported continuous functions are dense in L2L^2, the error term can be made arbitrarily small.

Formalization Note. Rd\mathbb R^d is EuclideanSpace ℝ (Fin d) with Lebesgue measure volume. K^\hat K is Lp.fourierTransformₗᵢ applied to hK.toLp K; the bound BB enters as ENNReal.ofReal B. The integral is the Bochner integral and norms are eLpNorm in ℝ≥0∞.

Preamble
import Mathlib.Analysis.Fourier.LpSpace
Formal statement
namespace DbarRegularity

open MeasureTheory FourierTransform Filter Topology
open scoped ENNReal NNReal Convolution

/-- The `L²` bound for `f ∈ L¹ ∩ L²`, up to an error controlled by a compactly supported
continuous approximation `K'` of `K`. -/
theorem eLpNorm_conv_le_aux {d : ℕ} (K : EuclideanSpace ℝ (Fin d) → ℂ) (hK : MemLp K 2 volume) (B : ℝ)
    (hB : ∀ᵐ ξ, ‖Lp.fourierTransformₗᵢ (EuclideanSpace ℝ (Fin d)) ℂ (hK.toLp K) ξ‖ ≤ B)
    (f : EuclideanSpace ℝ (Fin d) → ℂ) (hf1 : Integrable f volume) (hf2 : MemLp f 2 volume)
    (K' : EuclideanSpace ℝ (Fin d) → ℂ) (hK'c : Continuous K') (hK's : HasCompactSupport K')
    (hK'2 : MemLp K' 2 volume) :
    eLpNorm (fun x => ∫ y, K (x - y) * f y) 2 volume ≤
      ENNReal.ofReal B * eLpNorm f 2 volume +
        2 * (eLpNorm (K - K') 2 volume * eLpNorm f 1 volume) := by sorry

end DbarRegularity
Source
E. M. Stein, Singular Integrals and Differentiability Properties of Functions, Princeton University Press (1970), Chapter II, § 2.2, p. 29

View graph