Restricted interpolation with almost-everywhere sublinearity #
This version of the restricted interpolation argument permits null exceptional
sets in sublinearity. The tail containment is interpreted modulo null sets;
the truncations, layer-cake argument, and numerical constant are unchanged
from Foundation.Euclidean.InterpolationRestricted.
The layer-cake integration #
theorem
CKN.Core.Endgame.interpolation_weak11_strong22_of_l2_classes_ae
{T : (Foundation.Parabolic.Vec3 → ℝ) → Foundation.Parabolic.Vec3 → ℝ}
{A₁ A₂ p : ℝ}
(hTsub :
∀ (f g : Foundation.Parabolic.Vec3 → ℝ),
Measurable f →
MeasureTheory.Integrable f MeasureTheory.volume →
MeasureTheory.MemLp f 2 MeasureTheory.volume →
Measurable g →
MeasureTheory.MemLp g 2 MeasureTheory.volume →
∀ᵐ (x : Foundation.Parabolic.Vec3), |T (f + g) x| ≤ |T f x| + |T g x|)
(hTmeas :
∀ (f : Foundation.Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.MemLp f 2 MeasureTheory.volume → Measurable (T f))
(hweak :
∀ (f : Foundation.Parabolic.Vec3 → ℝ),
Measurable f →
MeasureTheory.Integrable f MeasureTheory.volume →
MeasureTheory.MemLp f 2 MeasureTheory.volume →
∀ (l : ℝ),
0 < l →
MeasureTheory.volume {x : Foundation.Parabolic.Vec3 | l < |T f x|} ≤ (ENNReal.ofReal A₁ * ∫⁻ (x : Foundation.Parabolic.Vec3), Foundation.Euclidean.absE f x) / ENNReal.ofReal l)
(hstrong :
∀ (f : Foundation.Parabolic.Vec3 → ℝ),
Measurable f →
MeasureTheory.MemLp f 2 MeasureTheory.volume →
∫⁻ (x : Foundation.Parabolic.Vec3), Foundation.Euclidean.absE (T f) x ^ 2 ≤ ENNReal.ofReal (A₂ ^ 2) * ∫⁻ (x : Foundation.Parabolic.Vec3), Foundation.Euclidean.absE f x ^ 2)
(hA₁ : 0 ≤ A₁)
(hp1 : 1 < p)
(hp2 : p < 2)
{f : Foundation.Parabolic.Vec3 → ℝ}
(hf : Measurable f)
(hfp : MeasureTheory.MemLp f (ENNReal.ofReal p) MeasureTheory.volume)
(hf2 : MeasureTheory.MemLp f 2 MeasureTheory.volume)
:
∫⁻ (x : Foundation.Parabolic.Vec3), Foundation.Euclidean.absE (T f) x ^ p ≤ ENNReal.ofReal (p * (2 ^ p * (A₁ / (p - 1) + A₂ ^ 2 / (2 - p)))) * ∫⁻ (x : Foundation.Parabolic.Vec3), Foundation.Euclidean.absE f x ^ p
Restricted weak and strong endpoint bounds interpolate when sublinearity holds almost everywhere on the actual L² input class.