Prove2Me

Convolution with an L2L^2 kernel of a sum of disjointly supported L1L^1 functions is a.e. bounded by the sum of the convolutions

Proved
DbarRegularity.ae_enorm_integral_mul_tsum_le

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

convolutionharmonic-analysismeasure-theory

Let d≥0d\ge0 and K∈L2(Rd)K\in L^2(\mathbb R^d), complex valued. Let (bk)k∈I(b_k)_{k\in I} be a countable family of integrable functions Rd→C\mathbb R^d\to\mathbb C with pairwise disjoint supports (no point has bk(x)≠0b_k(x)\ne0 and bl(x)≠0b_l(x)\ne0 with k≠lk\ne l), and suppose ∑kbk\sum_kb_k is integrable. Then for almost every x∈Rdx\in\mathbb R^d

∣∫K(x−y)∑kbk(y) dy∣  ≤  ∑k∣∫K(x−y) bk(y) dy∣.\Big|\int K(x-y)\sum_kb_k(y)\,dy\Big|\;\le\;\sum_k\Big|\int K(x-y)\,b_k(y)\,dy\Big| .

This controls convolution with an L2L^2 kernel applied to the bad part of a Calderón–Zygmund splitting by the sum of its actions on the individual pieces.

Formalization Note. Rd\mathbb R^d is EuclideanSpace ℝ (Fin d) with Lebesgue measure volume. The index type ι : Type is Countable, and ∑k\sum_k is tsum. The inequality is between extended nonnegative reals (‖·‖ₑ, with the right side a tsum in ℝ≥0∞). The integrals are Bochner integrals, which are 00 where the integrand is not integrable.

Preamble
import Definitions.Def_DbarRegularity_Setting
import Mathlib.MeasureTheory.Function.LpSeminorm.Basic
import Mathlib.MeasureTheory.Integral.Bochner.Basic
import Mathlib.Analysis.InnerProductSpace.PiL2
Formal statement
namespace DbarRegularity

open MeasureTheory
open scoped ENNReal

/-- For `K ∈ L²(ℝ^d)` and integrable functions `bₖ` with pairwise disjoint supports and integrable
sum, almost everywhere `|K * ∑ₖ bₖ| ≤ ∑ₖ |K * bₖ|`. -/
theorem ae_enorm_integral_mul_tsum_le {d : ℕ} {K : EuclideanSpace ℝ (Fin d) → ℂ}
    (hK : MemLp K 2 volume) {ι : Type} [Countable ι] (b : ι → EuclideanSpace ℝ (Fin d) → ℂ)
    (hb : ∀ k, Integrable (b k) volume) (hdisj : ∀ x k l, b k x ≠ 0 → b l x ≠ 0 → k = l)
    (hB : Integrable (fun x => ∑' k, b k x) volume) :
    ∀ᵐ x, ‖∫ y, K (x - y) * ∑' k, b k y‖ₑ ≤ ∑' k, ‖∫ y, K (x - y) * b k y‖ₑ := by sorry

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

View graph