Tonelli's Theorem for Nonnegative Functions #
These are the core statements of Tonelli's theorem that we need for the convolution case.
Tonelli's Theorem: Integral Equality on Product Measures
For a measurable nonnegative function on a product space, the double integral equals the iterated integral (in any order).
This is the fundamental statement: If f : G × G → ℝ≥0∞ is measurable and nonnegative, then: ∫⁻ (x,y), f (x,y) ∂(μ.prod μ) = ∫⁻ x, ∫⁻ y, f (x,y) ∂μ ∂μ
Section Finiteness from Product Finiteness (Tonelli Consequence)
If ∫⁻ (x,y), f (x,y) ∂(μ.prod μ) < ∞ where f is measurable and nonnegative, then for a.e. x, we have ∫⁻ y, f (x,y) ∂μ < ∞.
This is the key consequence of Tonelli for our application.
Tonelli for Norm Products (Nonnegative)
For measurable nonnegative functions f, g : G → ℝ≥0∞,
if ∫⁻ (x, y), f x * g y ∂(μ.prod μ) < ∞,
then for a.e. x, ∫⁻ y, f x * g y ∂μ < ∞.
Tonelli for Convolution Kernels #
These theorems apply Tonelli directly to the convolution kernel case.
Tonelli for Norm Convolution Kernels (Key Application)
For f, g : G → ℂ and measurable norms, if (x,y) ↦ f(x - y) * g(y) is integrable on μ.prod μ, then for a.e. x, y ↦ ‖f(x - y)‖ * ‖g(y)‖ is integrable on μ.
This theorem bridges from the product-level assumption to the section-level conclusion.
Tonelli for Real-Valued Convolution Kernels
For f, g : G → ℝ and nonnegative values, if (x,y) ↦ f(x - y) * g(y) has finite double integral, then for a.e. x, the section has finite integral.
Tonelli's Theorem: Product Decomposition #
Finer-grained versions of Tonelli that separate the roles of f and g.
Tonelli: Separate Factors
For f, g : G → ℂ with appropriate boundedness and a translation-invariant measure μ, ∫⁻ (x,y), ‖f(x-y) * g(y)‖ ∂(μ.prod μ) ≤ (∫⁻ x, ‖f x‖ ∂μ) * (∫⁻ y, ‖g y‖ ∂μ)
when these integrals are finite.
Auxiliary a.e.-finiteness lemmas for ℝ≥0∞-valued kernels assuming only
AEMeasurable on the product space. Proofs will be supplied where used.
From product finiteness for an AEMeasurable nonnegative kernel on μ.prod μ,
deduce that for a.e. x, the section y ↦ f (x, y) has finite lintegral.
Symmetric version: from product finiteness for an AEMeasurable nonnegative kernel,
deduce that for a.e. y, the section x ↦ f (x, y) has finite lintegral.
From product finiteness for an AEMeasurable nonnegative real-valued kernel on μ.prod μ,
deduce that for a.e. x, the section y ↦ H (x, y) is Bochner integrable (as an ℝ-valued
function).
From product finiteness for an AEMeasurable nonnegative real-valued kernel on μ.prod μ,
deduce that the outer integral x ↦ ∫ y, H (x, y) dμ is Bochner integrable on μ.
Fiberwise integrability for L²×L¹ convolution kernels.
Tonelli's theorem for nonnegative real-valued functions on a product space:
the lintegral of ENNReal.ofReal ∘ H on μ.prod μ equals ENNReal.ofReal of the
iterated Bochner integral when H is nonnegative and AEMeasurable.
This bridges the gap between ENNReal-valued lintegrals and real-valued iterated integrals.
Upper bound version of Tonelli for nonnegative functions:
the lintegral of ENNReal.ofReal ∘ H equals ENNReal.ofReal of the iterated integral
when H is nonnegative, AEMeasurable, and has finite lintegral.