Pressure slices with an actual weak gradient

The particular gradient is supplied as a measurable field with its weak identity. Only the test functions are differentiated classically.

theorem CKN.Core.Endgame.weak_partial_deriv_of_ae_sum {B : Set Foundation.Parabolic.Vec3} (hB : IsOpen B) {p P H gp gh : Foundation.Parabolic.Vec3 → ℝ} {k : Fin 3} (hrep : p =ᵐ[MeasureTheory.volume.restrict B] P + H) (hP : HasWeakPartialDerivOn B k P gp) (hH : HasWeakPartialDerivOn B k H gh) (hPloc : MeasureTheory.LocallyIntegrableOn P B MeasureTheory.volume) (hHloc : MeasureTheory.LocallyIntegrableOn H B MeasureTheory.volume) (hgploc : MeasureTheory.LocallyIntegrableOn gp B MeasureTheory.volume) (hghloc : MeasureTheory.LocallyIntegrableOn gh B MeasureTheory.volume) : HasWeakPartialDerivOn B k p (gp + gh)

Addition of locally integrable weak derivatives respects an a.e. decomposition of the underlying pressure.

theorem CKN.Core.Endgame.weak_partial_deriv_on_of_global_pairing {B : Set Foundation.Parabolic.Vec3} (hB : IsOpen B) {P D : Foundation.Parabolic.Vec3 → ℝ} {k : Fin 3} (hweak : ∀ (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∫ (x : Foundation.Parabolic.Vec3), P x * spatialDeriv ψ k x = -∫ (x : Foundation.Parabolic.Vec3), D x * ψ x) : HasWeakPartialDerivOn B k P D

A whole-space weak pairing restricts to any open slice domain.

theorem CKN.Core.Endgame.pressure_slice_bound_of_weak_extension {B B' : Set Foundation.Parabolic.Vec3} (hB : IsOpen B) {p P H D gh G : Foundation.Parabolic.Vec3 → ℝ} {k : Fin 3} {ρ C : ℝ} (hrep : p =ᵐ[MeasureTheory.volume.restrict B] P + H) (hweak : ∀ (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∫ (x : Foundation.Parabolic.Vec3), P x * spatialDeriv ψ k x = -∫ (x : Foundation.Parabolic.Vec3), D x * ψ x) (hH : HasWeakPartialDerivOn B k H gh) (hPloc : MeasureTheory.LocallyIntegrableOn P B MeasureTheory.volume) (hHloc : MeasureTheory.LocallyIntegrableOn H B MeasureTheory.volume) (hDloc : MeasureTheory.LocallyIntegrableOn D B MeasureTheory.volume) (hghloc : MeasureTheory.LocallyIntegrableOn gh B MeasureTheory.volume) (hD : MeasureTheory.eLpNorm D (ENNReal.ofReal (6 / 5)) MeasureTheory.volume ≤ ENNReal.ofReal C * MeasureTheory.eLpNorm G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) (hgh : MeasureTheory.eLpNorm gh (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict B') ≤ ENNReal.ofReal C * ENNReal.ofReal (ρ ^ (-1 / 2)) * MeasureTheory.eLpNorm p (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict B)) : MeasureTheory.LocallyIntegrableOn (D + gh) B MeasureTheory.volume ∧ HasWeakPartialDerivOn B k p (D + gh) ∧ MeasureTheory.eLpNorm (D + gh) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict B') ≤ ENNReal.ofReal C * (MeasureTheory.eLpNorm G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume + ENNReal.ofReal (ρ ^ (-1 / 2)) * MeasureTheory.eLpNorm p (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict B))

The local pressure-gradient estimate consumes the selected weak field directly, without identifying it with a classical derivative of a potential.

theorem CKN.Core.Endgame.pressure_slice_bound_of_vector_weak_extension {B B' : Set Foundation.Parabolic.Vec3} (hB : IsOpen B) {p P H gh G : Foundation.Parabolic.Vec3 → ℝ} {D : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} {k : Fin 3} {ρ C : ℝ} (hrep : p =ᵐ[MeasureTheory.volume.restrict B] P + H) (hweak : ∀ (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∫ (x : Foundation.Parabolic.Vec3), P x * spatialDeriv ψ k x = -∫ (x : Foundation.Parabolic.Vec3), D x k * ψ x) (hH : HasWeakPartialDerivOn B k H gh) (hPloc : MeasureTheory.LocallyIntegrableOn P B MeasureTheory.volume) (hHloc : MeasureTheory.LocallyIntegrableOn H B MeasureTheory.volume) (hDmem : MeasureTheory.MemLp D (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) (hghloc : MeasureTheory.LocallyIntegrableOn gh B MeasureTheory.volume) (hD : MeasureTheory.eLpNorm D (ENNReal.ofReal (6 / 5)) MeasureTheory.volume ≤ ENNReal.ofReal C * MeasureTheory.eLpNorm G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) (hgh : MeasureTheory.eLpNorm gh (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict B') ≤ ENNReal.ofReal C * ENNReal.ofReal (ρ ^ (-1 / 2)) * MeasureTheory.eLpNorm p (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict B)) : MeasureTheory.LocallyIntegrableOn (fun (x : Foundation.Parabolic.Vec3) => D x k + gh x) B MeasureTheory.volume ∧ (HasWeakPartialDerivOn B k p fun (x : Vec 3) => D x k + gh x) ∧ MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => D x k + gh x) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict B') ≤ ENNReal.ofReal C * (MeasureTheory.eLpNorm G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume + ENNReal.ofReal (ρ ^ (-1 / 2)) * MeasureTheory.eLpNorm p (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict B))

A vector-valued weak extension supplies each scalar slice estimate; local integrability of its coordinates follows from actual Lp membership.