Pressure Gradient Origin Clause Pairing

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

The origin clause as a full-space pairing

Clause (OC) of the paper is stated as an iterated pairing, first in space and then in time, against a smooth compactly supported test function carried by a product box B' ×ˢ J. The transfer lemmas downstream consume it instead as a single integral over the whole space-time carrier.

This file bridges the two shapes. Because the test function is supported in the box, the spatial gradient of the test function is supported there as well, so both integrands vanish outside B' ×ˢ J. Fubini on the product box, applied to the two integrable products, therefore identifies the box integral with the iterated one, and the box may be replaced by the whole carrier without changing either side.

theorem CKN.Core.Step4.originClause_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

Full-space form of the origin clause.

If the iterated space-time pairing identity ∫_J ∫_{B'} p ∂ᵢψ = -∫_J ∫_{B'} D ψ holds for a smooth compactly supported ψ carried by the box B' ×ˢ J, with p and D integrable on that box, then the same identity holds as a single integral over the whole carrier: the box may be replaced by all of space-time on both sides.

The support hypothesis is what makes the replacement legitimate: ψ vanishes off the box, and so does its spatial derivative ∂ᵢψ, since the latter is supported inside the support of ψ.