Restricted raw-function bounds for the L² operator #
The completed-space estimates transfer to raw representatives on the L² carrier. Additivity and sublinearity are asserted only almost everywhere; no algebraic property of the definition outside L² is used.
theorem
CKN.Core.Endgame.raw_rieszSecond_strong_two
{i j : Fin 3}
(hL2 : Foundation.Euclidean.RieszSecondL2Input i j)
{f : Foundation.Parabolic.Vec3 → ℝ}
(hf : MeasureTheory.MemLp f 2 MeasureTheory.volume)
:
∫⁻ (x : Foundation.Parabolic.Vec3), Foundation.Euclidean.absE (Foundation.Euclidean.rieszSecondL2RawOperator hL2 f) x ^ 2 ≤ ENNReal.ofReal (1 ^ 2) * ∫⁻ (x : Foundation.Parabolic.Vec3), Foundation.Euclidean.absE f x ^ 2
The raw representative satisfies the strong (2,2) power-integral
estimate on its actual L² carrier.
theorem
CKN.Core.Endgame.raw_rieszSecond_add_ae
{i j : Fin 3}
(hL2 : Foundation.Euclidean.RieszSecondL2Input i j)
{f g : Foundation.Parabolic.Vec3 → ℝ}
(hf : MeasureTheory.MemLp f 2 MeasureTheory.volume)
(hg : MeasureTheory.MemLp g 2 MeasureTheory.volume)
:
The raw operator is additive a.e. for pairs of L² inputs.
theorem
CKN.Core.Endgame.raw_rieszSecond_congr_ae
{i j : Fin 3}
(hL2 : Foundation.Euclidean.RieszSecondL2Input i j)
{f g : Foundation.Parabolic.Vec3 → ℝ}
(hf : MeasureTheory.MemLp f 2 MeasureTheory.volume)
(hg : MeasureTheory.MemLp g 2 MeasureTheory.volume)
(hfg : f =ᵐ[MeasureTheory.volume] g)
:
Almost-everywhere equal L² inputs have almost-everywhere equal raw outputs.
theorem
CKN.Core.Endgame.raw_rieszSecond_smul_ae
{i j : Fin 3}
(hL2 : Foundation.Euclidean.RieszSecondL2Input i j)
(c : ℝ)
{f : Foundation.Parabolic.Vec3 → ℝ}
(hf : MeasureTheory.MemLp f 2 MeasureTheory.volume)
:
Scalar multiplication commutes a.e. with the raw operator on L² inputs.
theorem
CKN.Core.Endgame.raw_rieszSecond_sublinear_ae
{i j : Fin 3}
(hL2 : Foundation.Euclidean.RieszSecondL2Input i j)
{f g : Foundation.Parabolic.Vec3 → ℝ}
(hf : MeasureTheory.MemLp f 2 MeasureTheory.volume)
(hg : MeasureTheory.MemLp g 2 MeasureTheory.volume)
:
Restricted a.e. sublinearity follows from the actual L² additivity.
theorem
CKN.Core.Endgame.raw_rieszSecond_distributional_identity
{i j : Fin 3}
(hL2 : Foundation.Euclidean.RieszSecondL2Input i j)
{f ψ : Foundation.Parabolic.Vec3 → ℝ}
(hf : MeasureTheory.MemLp f 2 MeasureTheory.volume)
(hψ : ContDiff ℝ (↑⊤) ψ)
(hψc : HasCompactSupport ψ)
:
∫ (x : Foundation.Parabolic.Vec3), Foundation.Euclidean.rieszSecondL2RawOperator hL2 f x * spatialLaplacian ψ x = ∫ (x : Foundation.Parabolic.Vec3), f x * mixedSecond ψ i j x
The raw L² representative satisfies the concrete distributional pairing against every smooth compactly supported test function.