Weak gradients selected from the actual indexed extension

The completed L^(6/5) operator supplies its own membership and numerical bound. Its positive pairing with the first potential selects the negatively signed weak gradient, without any classical representative identification.

Weak pressure gradients from indexed extension bounds

The negatively signed extension supplies a weak gradient of the first Newtonian derivative potential. Only distributional pairings and Lp bounds are used; no classical derivative of a rough representative is identified.

theorem CKN.Core.Endgame.exists_weak_pressure_gradient_of_extension (Ccomp C_CZ : ℝ) (hCcomp : 0 ≤ Ccomp) (hconst : 3 * Ccomp ≤ C_CZ) (T : Fin 3 → Fin 3 → (Foundation.Parabolic.Vec3 → ℝ) → Foundation.Parabolic.Vec3 → ℝ) (hmem : ∀ (i j : Fin 3) (G : Foundation.Parabolic.Vec3 → ℝ), MeasureTheory.MemLp G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume → HasCompactSupport G → MeasureTheory.MemLp (T i j G) (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) (hbound : ∀ (i j : Fin 3) (G : Foundation.Parabolic.Vec3 → ℝ), MeasureTheory.MemLp G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume → HasCompactSupport G → MeasureTheory.eLpNorm (T i j G) (ENNReal.ofReal (6 / 5)) MeasureTheory.volume ≤ ENNReal.ofReal Ccomp * MeasureTheory.eLpNorm G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) (hpair : ∀ (i j : Fin 3) (G : Foundation.Parabolic.Vec3 → ℝ), MeasureTheory.MemLp G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume → HasCompactSupport G → ∀ (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∫ (x : Foundation.Parabolic.Vec3), pressureNewtonianDerivativePotential i G x * spatialDeriv ψ j x = ∫ (x : Foundation.Parabolic.Vec3), T i j G x * ψ x) (i : Fin 3) (G : Foundation.Parabolic.Vec3 → ℝ) : MeasureTheory.MemLp G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume → HasCompactSupport G → ∃ (D : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3), MeasureTheory.MemLp D (ENNReal.ofReal (6 / 5)) MeasureTheory.volume ∧ (∀ (j : Fin 3) (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∫ (x : Foundation.Parabolic.Vec3), pressureNewtonianDerivativePotential i G x * spatialDeriv ψ j x = -∫ (x : Foundation.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

Actual component membership, bounds, and positive extension pairings give the weak gradient with the negative sign and a uniform vector bound.

theorem CKN.Core.Endgame.exists_weak_pressure_gradient_of_riesz_extension (C_CZ : ℝ) (hconst : 3 * Foundation.Euclidean.czGradientComponentConstant Foundation.Euclidean.rieszSecondWeakTypeConstant 1 ≤ C_CZ) (hL2 : (i j : Fin 3) → Foundation.Euclidean.RieszSecondL2Input i j) (hWeak11 : ∀ (i j : Fin 3) (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 i j) f x|} ≤ (ENNReal.ofReal Foundation.Euclidean.rieszSecondWeakTypeConstant * ∫⁻ (x : Foundation.Parabolic.Vec3), Foundation.Euclidean.absE f x) / ENNReal.ofReal l) (hpair : ∀ (i j : Fin 3) (G : Foundation.Parabolic.Vec3 → ℝ), MeasureTheory.MemLp G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume → HasCompactSupport G → ∀ (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∫ (x : Foundation.Parabolic.Vec3), pressureNewtonianDerivativePotential i G x * spatialDeriv ψ j x = ∫ (x : Foundation.Parabolic.Vec3), Foundation.Euclidean.rieszSecondGradientExtensionOperator (hL2 i j) ⋯ G x * ψ x) (i : Fin 3) (G : Foundation.Parabolic.Vec3 → ℝ) : MeasureTheory.MemLp G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume → HasCompactSupport G → ∃ (D : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3), MeasureTheory.MemLp D (ENNReal.ofReal (6 / 5)) MeasureTheory.volume ∧ (∀ (j : Fin 3) (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∫ (x : Foundation.Parabolic.Vec3), pressureNewtonianDerivativePotential i G x * spatialDeriv ψ j x = -∫ (x : Foundation.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 actual indexed extension produces the required weak-gradient output once its distributional pairing is supplied.