The completed gradient component on smooth compactly supported data

The completed L^(6/5) operator is built from the L² carrier by a norm-controlled extension, so on data that already lies in L² it reproduces the raw L² operator, and on smooth compactly supported data the raw operator is the classical Hessian ∂ᵢ∂ⱼ(N * G) of the Newtonian potential. This is the only place where a classical representative of the completed operator is identified, and it is used exactly on the dense class of test data.

theorem CKN.Foundation.Euclidean.rieszSecondGradientExtensionInput_T {i j : Fin 3} (hL2 : RieszSecondL2Input i j) (hWeak11 : ∀ (f : Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.Integrable f MeasureTheory.volume → MeasureTheory.MemLp f 2 MeasureTheory.volume → ∀ (l : ℝ), 0 < l → MeasureTheory.volume {x : Parabolic.Vec3 | l < |rieszSecondL2RawOperator hL2 f x|} ≤ (ENNReal.ofReal rieszSecondWeakTypeConstant * ∫⁻ (x : Parabolic.Vec3), absE f x) / ENNReal.ofReal l) : (rieszSecondGradientExtensionInput hL2 hWeak11).T = rieszSecondL2RawOperator hL2

The underlying map of the exponent 6 / 5 extension input is the raw L² operator.

theorem CKN.Foundation.Euclidean.rieszSecondGradientExtensionOperator_ae_raw {i j : Fin 3} (hL2 : RieszSecondL2Input i j) (hWeak11 : ∀ (f : Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.Integrable f MeasureTheory.volume → MeasureTheory.MemLp f 2 MeasureTheory.volume → ∀ (l : ℝ), 0 < l → MeasureTheory.volume {x : Parabolic.Vec3 | l < |rieszSecondL2RawOperator hL2 f x|} ≤ (ENNReal.ofReal rieszSecondWeakTypeConstant * ∫⁻ (x : Parabolic.Vec3), absE f x) / ENNReal.ofReal l) {f : Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) (hf₂ : MeasureTheory.MemLp f 2 MeasureTheory.volume) : rieszSecondGradientExtensionOperator hL2 hWeak11 f =ᵐ[MeasureTheory.volume] rieszSecondL2RawOperator hL2 f

On data lying in both L^(6/5) and L² the completed operator agrees almost everywhere with the raw L² operator.

theorem CKN.Foundation.Euclidean.rieszSecondGradientExtension_smooth_ae {i j : Fin 3} (hL2 : RieszSecondL2Input i j) (hWeak11 : ∀ (f : Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.Integrable f MeasureTheory.volume → MeasureTheory.MemLp f 2 MeasureTheory.volume → ∀ (l : ℝ), 0 < l → MeasureTheory.volume {x : Parabolic.Vec3 | l < |rieszSecondL2RawOperator hL2 f x|} ≤ (ENNReal.ofReal rieszSecondWeakTypeConstant * ∫⁻ (x : Parabolic.Vec3), absE f x) / ENNReal.ofReal l) {G : Parabolic.Vec3 → ℝ} (hG : ContDiff ℝ (↑⊤) G) (hGc : HasCompactSupport G) : rieszSecondGradientExtensionOperator hL2 hWeak11 G =ᵐ[MeasureTheory.volume] mixedSecond (pressureNewtonianPotential G) i j

On smooth compactly supported data the completed gradient component is the classical Hessian ∂ᵢ∂ⱼ(N * G) of the Newtonian potential.