Space-time pressure pairing for an identified slice field

Integrability of the same selected field on the inner carrier upgrades its slice weak derivative identity to the full-space test-function pairing.

theorem CKN.Core.Step4.pressure_pairing_of_integrable_slice_derivative {B : Set Foundation.Parabolic.Vec3} {J : Set ℝ} {p D : Foundation.Parabolic.ParabolicPoint → ℝ} (i : Fin 3) (hp : MeasureTheory.IntegrableOn p (B ×ˢ J) MeasureTheory.volume) (hD : MeasureTheory.IntegrableOn D (B ×ˢ J) MeasureTheory.volume) (hweak : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict J, HasWeakPartialDerivOn B i (fun (x : Vec 3) => p (x, s)) fun (x : Vec 3) => D (x, s)) {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hψs : tsupport ψ ⊆ B ×ˢ J) : ∫ (z : Foundation.Parabolic.ParabolicPoint), p z * spatialPartial ψ i z = -∫ (z : Foundation.Parabolic.ParabolicPoint), D z * ψ z

An integrable slice derivative satisfies the space-time pairing for every test function compactly supported in its product carrier.

theorem CKN.Core.Step4.inner_pressure_ball_eq_product (z₀ : Foundation.Parabolic.ParabolicPoint) (R : ℝ) : Metric.ball z₀ (R / 2) = Foundation.Parabolic.vec3Ball z₀.1 (R / 2) ×ˢ Set.Ioo (z₀.2 - R ^ 2 / 4) (z₀.2 + R ^ 2 / 4)

The inner symmetric metric ball is the exact spatial-time product used by the selected weak pressure derivative.