Lp Extension Exterior

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

noncomputable def CKN.Foundation.Euclidean.lpExtensionExteriorExteriorKernel (i j : Fin 3) : Parabolic.Vec3 → ℝ

Negative second spatial derivative of the Newtonian kernel for the exterior representation.

Equations

• CKN.Foundation.Euclidean.lpExtensionExteriorExteriorKernel i j = -CKN.spatialDeriv (CKN.spatialDeriv CKN.Foundation.Heat.newtonianKernel i) j

theorem CKN.Foundation.Euclidean.rieszSecondP1ExtensionOperator_agrees_exterior {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 : MeasureTheory.MemLp G (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) (hGc : HasCompactSupport G) {A U : Set Parabolic.Vec3} (hU : IsOpen U) (hGA : ∀ y ∉ A, G y = 0) (hAb : Bornology.IsBounded A) {δ : ℝ} (hδ : 0 < δ) (hsep : ∀ x ∈ U, ∀ y ∈ A, δ ≤ Parabolic.vec3EuclideanNorm (x - y)) : rieszSecondP1ExtensionOperator hL2 hWeak11 G =ᵐ[MeasureTheory.volume.restrict U] fun (x : Parabolic.Vec3) => ∫ (y : Parabolic.Vec3), (-spatialDeriv (spatialDeriv Heat.newtonianKernel i) j) (x - y) * G y

theorem CKN.Foundation.Euclidean.rieszSecondGradientExtensionOperator_agrees_exterior {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 : MeasureTheory.MemLp G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) (hGc : HasCompactSupport G) {A U : Set Parabolic.Vec3} (hU : IsOpen U) (hGA : ∀ y ∉ A, G y = 0) (hAb : Bornology.IsBounded A) {δ : ℝ} (hδ : 0 < δ) (hsep : ∀ x ∈ U, ∀ y ∈ A, δ ≤ Parabolic.vec3EuclideanNorm (x - y)) : rieszSecondGradientExtensionOperator hL2 hWeak11 G =ᵐ[MeasureTheory.volume.restrict U] fun (x : Parabolic.Vec3) => ∫ (y : Parabolic.Vec3), (-spatialDeriv (spatialDeriv Heat.newtonianKernel i) j) (x - y) * G y

theorem CKN.Foundation.Euclidean.pressureSecondExtensionOperator_agrees_exterior (hL2 : (i j : Fin 3) → RieszSecondL2Input i j) (hWeak11 : ∀ (i j : Fin 3) (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 i j) f x|} ≤ (ENNReal.ofReal rieszSecondWeakTypeConstant * ∫⁻ (x : Parabolic.Vec3), absE f x) / ENNReal.ofReal l) {G : Fin 3 → Fin 3 → Parabolic.Vec3 → ℝ} (hG : ∀ (i j : Fin 3), MeasureTheory.MemLp (G i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) (hGc : ∀ (i j : Fin 3), HasCompactSupport (G i j)) {A U : Set Parabolic.Vec3} (hU : IsOpen U) (hGA : ∀ (i j : Fin 3), ∀ y ∉ A, G i j y = 0) (hAb : Bornology.IsBounded A) {δ : ℝ} (hδ : 0 < δ) (hsep : ∀ x ∈ U, ∀ y ∈ A, δ ≤ Parabolic.vec3EuclideanNorm (x - y)) : pressureSecondExtensionOperator hL2 hWeak11 G =ᵐ[MeasureTheory.volume.restrict U] fun (x : Parabolic.Vec3) => ∑ i : Fin 3, ∑ j : Fin 3, ∫ (y : Parabolic.Vec3), (-spatialDeriv (spatialDeriv Heat.newtonianKernel i) j) (x - y) * G i j y