A jointly measurable space-time weak gradient from slice-wise weak gradients

Lemma lem:delta-p of the paper produces, for almost every time t, a spatial weak derivative of the pressure slice p (·, t) on a ball B. Nothing in that statement says that the family of slice derivatives can be chosen jointly measurable in space and time, and the almost-everywhere uniqueness of a weak derivative pins each slice down only up to a null set of its own. The theorems below supply the missing selection.

The construction is a mollification. With φ n the normalized bump of outer radius sliceRadius n and inner radius half of that, the function

G n (x, t) = ∫ y, (∂ₖ φ n) y * p (x - y, t) dy

is an explicit integral of a jointly measurable integrand, hence jointly measurable; and for each good time t and each x whose closed sliceRadius n-ball stays inside the domain, the defining integration-by-parts identity of HasWeakPartialDerivOn turns it into the mollification of the slice derivative at x. Mathlib's almost-everywhere convergence of mollifications (External Input ext:mollify) then makes G n (x, t) converge to the slice derivative at x for almost every x, so the pointwise limit

Dp z = limUnder atTop (fun n => G n z)

is a single space-time function that restricts to a weak derivative on almost every slice. The limit is Filter.limUnder, whose junk value off the convergence set is harmless: every conclusion is stated almost everywhere on the inner box.

The identity in the last conclusion is first proved in its iterated form ∫ t in J, ∫ x in B', which needs no integrability of Dp at all; setIntegral_prod_eq_of_iterated upgrades it to an integral over the product box once both integrands are integrable there.

The data is truncated to an intermediate open set W with closure B' ⊆ W ⊆ closure W ⊆ B before it is mollified, so that the truncated slices are globally integrable and Mathlib's convergence theorem applies; only the conclusions on B' are used.

Space-time points use the ordinary product space Vec3 × ℝ of docs/DESIGN_NOTES.md, the carrier on which spatialPartial and spaceTimeTestFunction are stated.

theorem CKN.exists_open_between_of_isCompact {d : ℕ} {s t : Set (Vec d)} (hs : IsCompact s) (ht : IsOpen t) (hst : s ⊆ t) : ∃ (W : Set (Vec d)) (δ : ℝ), 0 < δ ∧ IsOpen W ∧ s ⊆ W ∧ IsCompact (closure W) ∧ closure W ⊆ t ∧ ∀ x ∈ s, ∀ (ε : ℝ), 0 < ε → ε ≤ δ → Metric.closedBall x ε ⊆ W

Between a compact set and an open neighbourhood there is an open set W whose closure is a compact subset of the neighbourhood, and a radius δ such that every closed ball of radius at most δ centred on the compact set is contained in W.

theorem CKN.isCompact_slice_of_isCompact {K : Set (Foundation.Parabolic.Vec3 × ℝ)} (hK : IsCompact K) (t : ℝ) : IsCompact {x : Foundation.Parabolic.Vec3 | (x, t) ∈ K}

A spatial slice of a compact space-time set is compact.

theorem CKN.slice_testFunction {Ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} {B' : Set Foundation.Parabolic.Vec3} {J : Set ℝ} (hΨ : ContDiff ℝ (↑⊤) Ψ) (hΨc : HasCompactSupport Ψ) (hΨs : tsupport Ψ ⊆ B' ×ˢ J) (t : ℝ) : (ContDiff ℝ ↑⊤ fun (x : Foundation.Parabolic.Vec3) => Ψ (x, t)) ∧ (HasCompactSupport fun (x : Foundation.Parabolic.Vec3) => Ψ (x, t)) ∧ (tsupport fun (x : Foundation.Parabolic.Vec3) => Ψ (x, t)) ⊆ B'

The spatial slice of a space-time test function is a spatial test function.

theorem CKN.setIntegral_prod_eq_of_iterated {B' : Set Foundation.Parabolic.Vec3} {J : Set ℝ} {F H : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hF : MeasureTheory.IntegrableOn F (B' ×ˢ J) MeasureTheory.volume) (hH : MeasureTheory.IntegrableOn H (B' ×ˢ J) MeasureTheory.volume) (h : ∫ (t : ℝ) in J, ∫ (x : Foundation.Parabolic.Vec3) in B', F (x, t) = -∫ (t : ℝ) in J, ∫ (x : Foundation.Parabolic.Vec3) in B', H (x, t)) : ∫ (z : Foundation.Parabolic.Vec3 × ℝ) in B' ×ˢ J, F z = -∫ (z : Foundation.Parabolic.Vec3 × ℝ) in B' ×ˢ J, H z

The iterated space-time identity becomes an identity of integrals over the product box as soon as both integrands are integrable there.

theorem CKN.exists_spacetime_weak_gradient_of_slices (k : Fin 3) {B B' : Set Foundation.Parabolic.Vec3} {J : Set ℝ} {p : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hB : IsOpen B) (hB' : MeasurableSet B') (hB'c : IsCompact (closure B')) (hB'B : closure B' ⊆ B) (hp : MeasureTheory.IntegrableOn p (B ×ˢ J) MeasureTheory.volume) (hslice : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict J, ∃ (g : Foundation.Parabolic.Vec3 → ℝ), MeasureTheory.LocallyIntegrableOn g B MeasureTheory.volume ∧ HasWeakPartialDerivOn B k (fun (x : Vec 3) => p (x, t)) g) : ∃ (Dp : Foundation.Parabolic.Vec3 × ℝ → ℝ), AEMeasurable Dp (MeasureTheory.volume.restrict (B' ×ˢ J)) ∧ (∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict J, ∀ (g : Foundation.Parabolic.Vec3 → ℝ), MeasureTheory.LocallyIntegrableOn g B MeasureTheory.volume → HasWeakPartialDerivOn B k (fun (x : Vec 3) => p (x, t)) g → (fun (x : Foundation.Parabolic.Vec3) => Dp (x, t)) =ᵐ[MeasureTheory.volume.restrict B'] g) ∧ (∀ (Ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) Ψ → HasCompactSupport Ψ → tsupport Ψ ⊆ B' ×ˢ J → ∫ (t : ℝ) in J, ∫ (x : Foundation.Parabolic.Vec3) in B', p (x, t) * spatialPartial Ψ k (x, t) = -∫ (t : ℝ) in J, ∫ (x : Foundation.Parabolic.Vec3) in B', Dp (x, t) * Ψ (x, t)) ∧ ∀ (Ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) Ψ → HasCompactSupport Ψ → tsupport Ψ ⊆ B' ×ˢ J → MeasureTheory.IntegrableOn (fun (z : Foundation.Parabolic.Vec3 × ℝ) => p z * spatialPartial Ψ k z) (B' ×ˢ J) MeasureTheory.volume → MeasureTheory.IntegrableOn (fun (z : Foundation.Parabolic.Vec3 × ℝ) => Dp z * Ψ z) (B' ×ˢ J) MeasureTheory.volume → ∫ (z : Foundation.Parabolic.Vec3 × ℝ) in B' ×ˢ J, p z * spatialPartial Ψ k z = -∫ (z : Foundation.Parabolic.Vec3 × ℝ) in B' ×ˢ J, Dp z * Ψ z

Existence of a jointly measurable space-time weak spatial derivative, given slice-wise weak derivatives for almost every time. The four conclusions are joint measurability on the inner box, identification with every slice weak derivative on the inner set at almost every time, the iterated space-time integration-by-parts identity against test functions supported in the inner box, and the same identity over the product box whenever both integrands are integrable there. The slice hypothesis is the one produced by lem:delta-p: the test-function identity of HasWeakPartialDerivOn, holding for almost every time with a locally integrable derivative on the outer set B.