Marcinkiewicz interpolation between weak (1,1) and strong (2,2)

This file develops the analytic ingredients for the Marcinkiewicz interpolation theorem in the range 1 < p < 2 for a sublinear operator T on functions Vec3 → ℝ that is of weak type (1,1) with constant A₁ and of strong type (2,2) with constant A₂. The distribution-function estimate |{x | |T f x| > 2λ}| ≤ A₁ ‖f·1_{|f|>λ}‖₁/λ + A₂² ‖f·1_{|f|≤λ}‖₂²/λ² and its integral against the layer-cake weight p t^{p-1} are proven here; the interpolation theorem itself, with the explicit constant p · 2^p · (A₁/(p-1) + A₂²/(2-p)), is interpolation_weak11_strong22 in Interpolation.lean.

The proof works throughout with Lebesgue integrals in ℝ≥0∞; measurability of the input function and of its image under T are explicit hypotheses.

noncomputable def CKN.Foundation.Euclidean.rpowExt (a t : ℝ) : ℝ

A measurable replacement for the real power t ^ a, equal to it for t > 0 and vanishing for t ≤ 0. It is used so that the weights occurring in the layer-cake integrals are globally measurable.

Equations

• CKN.Foundation.Euclidean.rpowExt a t = if 0 < t then Real.exp (a * Real.log t) else 0

theorem CKN.Foundation.Euclidean.rpowExt_eq {a t : ℝ} (ht : 0 < t) : rpowExt a t = t ^ a

The high-frequency contribution

noncomputable def CKN.Foundation.Euclidean.weightedHighIntegrand (N : Parabolic.Vec3 → ENNReal) (p t : ℝ) (x : Parabolic.Vec3) : ENNReal

Weighted high-amplitude integrand used in the interpolation distribution-function argument.

Equations

• CKN.Foundation.Euclidean.weightedHighIntegrand N p t x = ENNReal.ofReal (CKN.Foundation.Euclidean.rpowExt (p - 2) t) * (N ⁻¹' Set.Ioi (ENNReal.ofReal (t / 2))).indicator N x

theorem CKN.Foundation.Euclidean.measurable_weightedHighIntegrand {N : Parabolic.Vec3 → ENNReal} (hN : Measurable N) {p : ℝ} : AEMeasurable (Function.uncurry (weightedHighIntegrand N p)) ((MeasureTheory.volume.restrict (Set.Ioi 0)).prod MeasureTheory.volume)

theorem CKN.Foundation.Euclidean.inner_High_eq {N : Parabolic.Vec3 → ENNReal} (hN : Measurable N) {p : ℝ} (t : ℝ) : ∫⁻ (x : Parabolic.Vec3), weightedHighIntegrand N p t x = ENNReal.ofReal (rpowExt (p - 2) t) * ∫⁻ (x : Parabolic.Vec3) in N ⁻¹' Set.Ioi (ENNReal.ofReal (t / 2)), N x

The low-frequency contribution

noncomputable def CKN.Foundation.Euclidean.weightedLowIntegrand (N : Parabolic.Vec3 → ENNReal) (p t : ℝ) (x : Parabolic.Vec3) : ENNReal

Weighted low-amplitude square integrand used in the interpolation argument.

Equations

• One or more equations did not get rendered due to their size.

The truncation at level t / 2 and the tail bound

def CKN.Foundation.Euclidean.absE (f : Parabolic.Vec3 → ℝ) : Parabolic.Vec3 → ENNReal

The ℝ≥0∞-valued modulus of a real function; it converts the real-valued weak- and strong-type hypotheses into inequalities between Lebesgue integrals.

Equations

• CKN.Foundation.Euclidean.absE f x = ENNReal.ofReal |f x|

theorem CKN.Foundation.Euclidean.measurable_absE {f : Parabolic.Vec3 → ℝ} (hf : Measurable f) : Measurable (absE f)

theorem CKN.Foundation.Euclidean.tail_bound {T : (Parabolic.Vec3 → ℝ) → Parabolic.Vec3 → ℝ} {A₁ A₂ : ℝ} (hTsub : ∀ (f g : Parabolic.Vec3 → ℝ) (x : Parabolic.Vec3), |T (f + g) x| ≤ |T f x| + |T g x|) (hTmeas : ∀ (f : Parabolic.Vec3 → ℝ), Measurable f → Measurable (T f)) (hweak : ∀ (f : Parabolic.Vec3 → ℝ), Measurable f → ∀ (l : ℝ), 0 < l → MeasureTheory.volume {x : Parabolic.Vec3 | l < |T f x|} ≤ (ENNReal.ofReal A₁ * ∫⁻ (x : Parabolic.Vec3), absE f x) / ENNReal.ofReal l) (hstrong : ∀ (f : Parabolic.Vec3 → ℝ), Measurable f → ∫⁻ (x : Parabolic.Vec3), absE (T f) x ^ 2 ≤ ENNReal.ofReal (A₂ ^ 2) * ∫⁻ (x : Parabolic.Vec3), absE f x ^ 2) {f : Parabolic.Vec3 → ℝ} (hf : Measurable f) {t : ℝ} (ht : 0 < t) : MeasureTheory.volume {x : Parabolic.Vec3 | t < |T f x|} ≤ (ENNReal.ofReal (2 * A₁ / t) * ∫⁻ (x : Parabolic.Vec3) in absE f ⁻¹' Set.Ioi (ENNReal.ofReal (t / 2)), absE f x) + ENNReal.ofReal (4 * A₂ ^ 2 / t ^ 2) * ∫⁻ (x : Parabolic.Vec3) in absE f ⁻¹' Set.Iic (ENNReal.ofReal (t / 2)), absE f x ^ 2

The distribution-function bound obtained by truncating f at the level t / 2: the weak (1,1) estimate controls the part of f above the level and the strong (2,2) estimate (via Chebyshev's inequality) the part below it.

The layer-cake weight and the interpolation constant

theorem CKN.Foundation.Euclidean.interp_integrand {A₁ A₂ p t : ℝ} (hA₁ : 0 ≤ A₁) (hp1 : 1 < p) (ht : 0 < t) (H L : ENNReal) : (ENNReal.ofReal (2 * A₁ / t) * H + ENNReal.ofReal (4 * A₂ ^ 2 / t ^ 2) * L) * ENNReal.ofReal (p * t ^ (p - 1)) = ENNReal.ofReal p * (ENNReal.ofReal (2 * A₁) * (ENNReal.ofReal (t ^ (p - 2)) * H) + ENNReal.ofReal (4 * A₂ ^ 2) * (ENNReal.ofReal (t ^ (p - 3)) * L))

The pointwise distribution-function inequality of the tail bound, rewritten as a product of the two layer-cake weights with the split coefficients.

The weighted layer-cake integral

noncomputable def CKN.Foundation.Euclidean.highTail (N : Parabolic.Vec3 → ENNReal) (t : ℝ) : ENNReal

The high-frequency tail integral ∫_{N > t/2} N, viewed as a function of the level t.

Equations

• CKN.Foundation.Euclidean.highTail N t = ∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in N ⁻¹' Set.Ioi (ENNReal.ofReal (t / 2)), N x

noncomputable def CKN.Foundation.Euclidean.lowTail (N : Parabolic.Vec3 → ENNReal) (t : ℝ) : ENNReal

The low-frequency tail integral ∫_{N ≤ t/2} N ^ 2, viewed as a function of the level t.

Equations

• CKN.Foundation.Euclidean.lowTail N t = ∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in N ⁻¹' Set.Iic (ENNReal.ofReal (t / 2)), N x ^ 2

theorem CKN.Foundation.Euclidean.layer_cake {T : (Parabolic.Vec3 → ℝ) → Parabolic.Vec3 → ℝ} {f : Parabolic.Vec3 → ℝ} (hTf : Measurable (T f)) {p : ℝ} (hp1 : 1 < p) : ∫⁻ (x : Parabolic.Vec3), absE (T f) x ^ p = ∫⁻ (t : ℝ) in Set.Ioi 0, MeasureTheory.volume {x : Parabolic.Vec3 | t < |T f x|} * ENNReal.ofReal (p * t ^ (p - 1))

The layer-cake representation of ∫ |T f| ^ p as the integral over the level t of the distribution function of |T f| against the weight p t ^ (p - 1).

theorem CKN.Foundation.Euclidean.weighted_combined {N : Parabolic.Vec3 → ENNReal} (hN : Measurable N) (hNfin : ∀ (x : Parabolic.Vec3), N x < ⊤) {A₁ A₂ p : ℝ} (hA₁ : 0 ≤ A₁) (hp1 : 1 < p) (hp2 : p < 2) : (∫⁻ (t : ℝ) in Set.Ioi 0, ENNReal.ofReal (2 * A₁) * (ENNReal.ofReal (rpowExt (p - 2) t) * highTail N t)) + ∫⁻ (t : ℝ) in Set.Ioi 0, ENNReal.ofReal (4 * A₂ ^ 2) * (ENNReal.ofReal (rpowExt (p - 3) t) * lowTail N t) = ENNReal.ofReal (2 ^ p * (A₁ / (p - 1) + A₂ ^ 2 / (2 - p))) * ∫⁻ (x : Parabolic.Vec3), N x ^ p

Evaluating the two weighted tail integrals of the distribution-function estimate against the layer-cake weight and collecting the coefficients into the interpolation constant.