Lp Extension CZ

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

theorem CKN.Foundation.Euclidean.hCZ_p1_of_rieszSecond_l2_extension {i j : Fin 3} {p₁ g : Parabolic.Vec3 → ℝ} {C_CZ E : ℝ} (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) (hg : MeasureTheory.MemLp g (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) (hgc : HasCompactSupport g) (hident : p₁ =ᵐ[MeasureTheory.volume] rieszSecondP1ExtensionOperator hL2 hWeak11 g) (hsource : MeasureTheory.lpNorm g (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ E ^ (2 / 3)) (hC_CZ : 0 ≤ C_CZ) (hconst : czP1Constant rieszSecondWeakTypeConstant 1 ≤ C_CZ) (hE : 0 ≤ E) : MeasureTheory.lpNorm p₁ (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ C_CZ * E ^ (2 / 3)

theorem CKN.Foundation.Euclidean.hCZ_grad_of_rieszSecond_l2_extension {C_CZ : ℝ} (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) (hconst : 3 * czGradientComponentConstant rieszSecondWeakTypeConstant 1 ≤ C_CZ) : HasCZGradientOperatorBound (fun (i j : Fin 3) (G : Parabolic.Vec3 → ℝ) (x : Parabolic.Vec3) => -rieszSecondGradientExtensionOperator (hL2 i j) ⋯ G x) C_CZ

theorem CKN.Foundation.Euclidean.exists_weak_pressure_gradient_of_rieszSecond_l2_extension (C_CZ : ℝ) (hconst : 3 * czGradientComponentConstant rieszSecondWeakTypeConstant 1 ≤ C_CZ) (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) (hpair : ∀ (i j : Fin 3) (G : Parabolic.Vec3 → ℝ), MeasureTheory.MemLp G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume → HasCompactSupport G → ∀ (ψ : Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∫ (x : Parabolic.Vec3), pressureNewtonianDerivativePotential i G x * spatialDeriv ψ j x = ∫ (x : Parabolic.Vec3), rieszSecondGradientExtensionOperator (hL2 i j) ⋯ G x * ψ x) (i : Fin 3) (G : Parabolic.Vec3 → ℝ) : MeasureTheory.MemLp G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume → HasCompactSupport G → ∃ (D : Parabolic.Vec3 → Parabolic.Vec3), MeasureTheory.MemLp D (ENNReal.ofReal (6 / 5)) MeasureTheory.volume ∧ (∀ (j : Fin 3) (ψ : Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∫ (x : Parabolic.Vec3), pressureNewtonianDerivativePotential i G x * spatialDeriv ψ j x = -∫ (x : Parabolic.Vec3), D x j * ψ x) ∧ MeasureTheory.eLpNorm D (ENNReal.ofReal (6 / 5)) MeasureTheory.volume ≤ ENNReal.ofReal C_CZ * MeasureTheory.eLpNorm G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume

Consume the positive pairing of the completed extension and return the selected negative weak-gradient field.

theorem CKN.Foundation.Euclidean.exists_weak_pressure_gradient_of_rieszSecond_l2_extension_unconditional (C_CZ : ℝ) (hconst : 3 * czGradientComponentConstant rieszSecondWeakTypeConstant 1 ≤ C_CZ) (i : Fin 3) (G : Parabolic.Vec3 → ℝ) : MeasureTheory.MemLp G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume → HasCompactSupport G → ∃ (D : Parabolic.Vec3 → Parabolic.Vec3), MeasureTheory.MemLp D (ENNReal.ofReal (6 / 5)) MeasureTheory.volume ∧ (∀ (j : Fin 3) (ψ : Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∫ (x : Parabolic.Vec3), pressureNewtonianDerivativePotential i G x * spatialDeriv ψ j x = -∫ (x : Parabolic.Vec3), D x j * ψ x) ∧ MeasureTheory.eLpNorm D (ENNReal.ofReal (6 / 5)) MeasureTheory.volume ≤ ENNReal.ofReal C_CZ * MeasureTheory.eLpNorm G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume

The completed weak-gradient output with concrete endpoint data and the positive pairing supplied by the extension theorem.

noncomputable def CKN.Foundation.Euclidean.rieszSecondP1ExtensionTensorOperator (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 → ℝ) : Parabolic.Vec3 → ℝ

Tensor second-Riesz operator at exponent three-halves, built from L² and weak-(1,1) data.

Equations

• One or more equations did not get rendered due to their size.

theorem CKN.Foundation.Euclidean.rieszSecondP1ExtensionTensor_memLp (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) : MeasureTheory.MemLp (rieszSecondP1ExtensionTensorOperator hL2 hWeak11 G) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume

theorem CKN.Foundation.Euclidean.rieszSecondP1ExtensionTensor_eLpNorm_le (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)) : MeasureTheory.eLpNorm (rieszSecondP1ExtensionTensorOperator hL2 hWeak11 G) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ ∑ i : Fin 3, ∑ j : Fin 3, ENNReal.ofReal (czP1Constant rieszSecondWeakTypeConstant 1) * MeasureTheory.eLpNorm (G i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume

theorem CKN.Foundation.Euclidean.pressure_lpNorm_le_of_rieszSecond_p1_tensor_extension {p₁ : Parabolic.Vec3 → ℝ} {E C_CZ : ℝ} (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)) (hident : p₁ =ᵐ[MeasureTheory.volume] rieszSecondP1ExtensionTensorOperator hL2 hWeak11 G) (hsource : ∑ i : Fin 3, ∑ j : Fin 3, MeasureTheory.lpNorm (G i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ E ^ (2 / 3)) (hconst : czP1Constant rieszSecondWeakTypeConstant 1 ≤ C_CZ) (hE : 0 ≤ E) : MeasureTheory.lpNorm p₁ (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ C_CZ * E ^ (2 / 3)