Documentation

TauCeti.MeasureTheory.Integral.SchurTest

Schur's test for integral operators #

Let k : α → β → ℝ≥0∞ be a jointly measurable kernel whose row integrals ∫⁻ y, k x y ∂ν are at most A and whose column integrals ∫⁻ x, k x y ∂μ are at most B. Then, for 1 ≤ p, the integral operator g ↦ (x ↦ ∫⁻ y, k x y * g y ∂ν) satisfies

∫⁻ x, (∫⁻ y, k x y * g y ∂ν) ^ p ∂μ ≤ A ^ (p - 1) * B * ∫⁻ y, g y ^ p ∂ν.

When A and B are finite, this says that it maps Lᵖ(ν) to Lᵖ(μ) with norm at most A ^ (1 - 1/p) * B ^ (1/p). For a translation-invariant kernel k x y = K (x - y) with K integrable this is Young's inequality for convolution with an L¹ function; a typical use is for weakly singular kernels such as ‖x - y‖ ^ (1 - n) restricted to a bounded set, which bound Riesz potentials in Lᵖ.

The proof applies Hölder's inequality, in the form TauCeti.rpow_lintegral_le_measure_univ_rpow_mul, to the measure ν.withDensity (k x) for each x, and then exchanges the order of integration by Tonelli's theorem.

The statement is in ℝ≥0∞, so it needs no integrability hypotheses, and the bounds on the row and column integrals are only required almost everywhere.

Main declarations #

References #

theorem TauCeti.lintegral_rpow_lintegral_mul_le {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] {k : α → β → ENNReal} (hk : Measurable (Function.uncurry k)) {g : β → ENNReal} (hg : AEMeasurable g ν) {p : ℝ} (hp : 1 ≤ p) {A B : ENNReal} (hA : ∀ᵐ (x : α) ∂μ, ∫⁻ (y : β), k x y ∂ν ≤ A) (hB : ∀ᵐ (y : β) ∂ν, ∫⁻ (x : α), k x y ∂μ ≤ B) :
∫⁻ (x : α), (∫⁻ (y : β), k x y * g y ∂ν) ^ p ∂μ ≤ A ^ (p - 1) * B * ∫⁻ (y : β), g y ^ p ∂ν

Schur's test. If the kernel k has row integrals ∫⁻ y, k x y ∂ν at most A for almost every x and column integrals ∫⁻ x, k x y ∂μ at most B for almost every y, then for 1 ≤ p the integral operator with kernel k satisfies ∫⁻ x, (∫⁻ y, k x y * g y ∂ν) ^ p ∂μ ≤ A ^ (p - 1) * B * ∫⁻ y, g y ^ p ∂ν.