Pressure Gradient Origin Cell Instance Pairing

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

An iterated space-time pairing identity on a product box upgrades to the full-space pairing whenever the test function is supported in that box. The smoothness and compact support of the spatial partial derivative are inherited from the test function, so the two full-space integrals collapse to their restrictions to the product box.

theorem CKN.Core.Step4.OriginInstance.spacetime_pairing_of_iterated {B' : Set Foundation.Parabolic.Vec3} {J : Set ℝ} {p D : Foundation.Parabolic.ParabolicPoint → ℝ} {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} {i : Fin 3} (hψ : ψ ∈ spaceTimeTestFunction Set.univ Set.univ) (hsupp : tsupport ψ ⊆ B' ×ˢ J) (hp : MeasureTheory.IntegrableOn p (B' ×ˢ J) MeasureTheory.volume) (hD : MeasureTheory.IntegrableOn D (B' ×ˢ J) MeasureTheory.volume) (hiter : ∫ (t : ℝ) in J, ∫ (x : Foundation.Parabolic.Vec3) in B', p (x, t) * spatialPartial ψ i (x, t) = -∫ (t : ℝ) in J, ∫ (x : Foundation.Parabolic.Vec3) in B', D (x, t) * ψ (x, t)) : ∫ (z : Foundation.Parabolic.ParabolicPoint), p z * spatialPartial ψ i z = -∫ (z : Foundation.Parabolic.ParabolicPoint), D z * ψ z

An iterated space-time pairing identity on a product box upgrades to the full-space pairing whenever the test function is supported in that box.