Interpolation of the actual raw L² operator #
The completed L² operator supplies measurability, a.e. sublinearity, and the strong endpoint. Only its restricted weak estimate remains an analytic input to the intermediate-exponent estimate.
theorem
CKN.Core.Endgame.raw_rieszSecond_interpolation_of_weak
{i j : Fin 3}
(hL2 : Foundation.Euclidean.RieszSecondL2Input i j)
{A₁ p : ℝ}
(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 < |Foundation.Euclidean.rieszSecondL2RawOperator hL2 f x|} ≤ (ENNReal.ofReal A₁ * ∫⁻ (x : Foundation.Parabolic.Vec3), Foundation.Euclidean.absE f x) / ENNReal.ofReal l)
(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)
:
The raw operator interpolates on the intersection of Lᵖ and L² using the actual L² endpoint and only a restricted weak estimate.
theorem
CKN.Core.Endgame.raw_rieszSecond_interpolation_of_weak_ae
{i j : Fin 3}
(hL2 : Foundation.Euclidean.RieszSecondL2Input i j)
{A₁ p : ℝ}
(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 < |Foundation.Euclidean.rieszSecondL2RawOperator hL2 f x|} ≤ (ENNReal.ofReal A₁ * ∫⁻ (x : Foundation.Parabolic.Vec3), Foundation.Euclidean.absE f x) / ENNReal.ofReal l)
(hA₁ : 0 ≤ A₁)
(hp1 : 1 < p)
(hp2 : p < 2)
{f : Foundation.Parabolic.Vec3 → ℝ}
(hfp : MeasureTheory.MemLp f (ENNReal.ofReal p) MeasureTheory.volume)
(hf2 : MeasureTheory.MemLp f 2 MeasureTheory.volume)
:
The intermediate power estimate respects a.e. representatives, so the original input needs only its two finite Lp memberships.
theorem
CKN.Core.Endgame.raw_rieszSecond_memLp_and_bound_of_weak
{i j : Fin 3}
(hL2 : Foundation.Euclidean.RieszSecondL2Input i j)
{A₁ p : ℝ}
(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 < |Foundation.Euclidean.rieszSecondL2RawOperator hL2 f x|} ≤ (ENNReal.ofReal A₁ * ∫⁻ (x : Foundation.Parabolic.Vec3), Foundation.Euclidean.absE f x) / ENNReal.ofReal l)
(hA₁ : 0 ≤ A₁)
(hp1 : 1 < p)
(hp2 : p < 2)
{f : Foundation.Parabolic.Vec3 → ℝ}
(hfp : MeasureTheory.MemLp f (ENNReal.ofReal p) MeasureTheory.volume)
(hf2 : MeasureTheory.MemLp f 2 MeasureTheory.volume)
:
MeasureTheory.MemLp (Foundation.Euclidean.rieszSecondL2RawOperator hL2 f) (ENNReal.ofReal p) MeasureTheory.volume ∧ MeasureTheory.eLpNorm (Foundation.Euclidean.rieszSecondL2RawOperator hL2 f) (ENNReal.ofReal p) MeasureTheory.volume ≤ ENNReal.ofReal (Foundation.Euclidean.rieszSecondInterpolationConstant A₁ 1 p) ^ (1 / p) * MeasureTheory.eLpNorm f (ENNReal.ofReal p) MeasureTheory.volume
The actual raw operator maps the dense intersection to Lᵖ and obeys the explicit interpolated seminorm estimate.
theorem
CKN.Core.Endgame.raw_rieszSecond_toLp_bound_of_weak
{i j : Fin 3}
(hL2 : Foundation.Euclidean.RieszSecondL2Input i j)
{A₁ p : ℝ}
(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 < |Foundation.Euclidean.rieszSecondL2RawOperator hL2 f x|} ≤ (ENNReal.ofReal A₁ * ∫⁻ (x : Foundation.Parabolic.Vec3), Foundation.Euclidean.absE f x) / ENNReal.ofReal l)
(hA₁ : 0 ≤ A₁)
(hp1 : 1 < p)
(hp2 : p < 2)
{f : Foundation.Parabolic.Vec3 → ℝ}
(hfp : MeasureTheory.MemLp f (ENNReal.ofReal p) MeasureTheory.volume)
(hf2 : MeasureTheory.MemLp f 2 MeasureTheory.volume)
(hTf :
MeasureTheory.MemLp (Foundation.Euclidean.rieszSecondL2RawOperator hL2 f) (ENNReal.ofReal p) MeasureTheory.volume)
:
The dense-class bound in the real Lp norm convention, with the same explicit interpolation coefficient.