The pointwise convolution integral $x\mapsto\int K(x-y)f(y)\,dy$ is a.e. strongly measurable

Proved

DbarRegularity.aestronglyMeasurable_integral_mul_sub

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

convolutionharmonic-analysismeasure-theory

Let $d\ge0$ and let $K,f:\mathbb R^d\to\mathbb C$ be almost-everywhere strongly measurable. Then the function

x\;\longmapsto\;\int_{\mathbb R^d}K(x-y)\,f(y)\,dy

is almost-everywhere strongly measurable on $\mathbb R^d$ .

No integrability is assumed: at points $x$ where $y\mapsto K(x-y)f(y)$ is not integrable the Bochner integral is $0$ by convention, and the statement still holds. This is the basic measurability fact for convolution operators $f\mapsto K*f$ defined pointwise by the integral.

Formalization Note. $\mathbb R^d$ is EuclideanSpace ℝ (Fin d) with Lebesgue measure volume; the integral is the Bochner integral ∫ y, K (x - y) * f y, which Lean sets to $0$ when the integrand is not integrable.

Preamble

import Mathlib.MeasureTheory.Integral.Prod
import Mathlib.MeasureTheory.Group.Prod
import Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
import Mathlib.Analysis.InnerProductSpace.PiL2

Formal statement

namespace DbarRegularity

open MeasureTheory
open scoped ENNReal

/-- The convolution-type integral `x ↦ ∫ K(x - y) f(y) dy` of a.e.-strongly measurable functions
is a.e.-strongly measurable. -/
theorem aestronglyMeasurable_integral_mul_sub {d : ℕ} (K f : EuclideanSpace ℝ (Fin d) → ℂ)
    (hK : AEStronglyMeasurable K volume) (hf : AEStronglyMeasurable f volume) :
    AEStronglyMeasurable (fun x => ∫ y, K (x - y) * f y) 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

The pointwise convolution integral x↦∫K(x−y)f(y) dyx\mapsto\int K(x-y)f(y)\,dyx↦∫K(x−y)f(y)dy is a.e. strongly measurable

The pointwise convolution integral $x\mapsto\int K(x-y)f(y)\,dy$ is a.e. strongly measurable