Space-time distributional identities restricted to time slices

Testing a space-time distributional identity against a product ψ(x)θ(t) of a spatial test function and a time cutoff and separating the variables gives, for each fixed ψ, a slice identity valid for almost every time. The exceptional null set produced this way depends on ψ.

This file removes that dependence. Starting from the family of slice identities indexed by ψ, the countable subfamily indexed by the mollifier bumps centred at the points of a countable dense set yields a single null set, and slice_pairing_zero_of_mollifier_family upgrades the countable family back to every test function. The result is the almost-everywhere slice statement used in paper/ckn.tex: for almost every time, the slice is divergence free in the sense of distributions, with one null set serving every test function.

The pairing covered is the spatial divergence pairing ∑ᵢ fᵢ ∂ᵢψ. Its full-space form is exactly the slice hypothesis consumed by the pressure module's force-cancellation results.

theorem CKN.ae_slice_divergence_zero_of_forall_test {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} (hΩ : IsOpen Ω) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hloc : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∀ (i : Fin 3), MeasureTheory.LocallyIntegrableOn (fun (x : Foundation.Parabolic.Vec3) => f (x, s) i) Ω MeasureTheory.volume) (hslice : ∀ (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ Ω → ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∫ (x : Foundation.Parabolic.Vec3) in Ω, ∑ i : Fin 3, f (x, s) i * (fderiv ℝ ψ x) (basisVec i) = 0) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∀ (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ Ω → ∫ (x : Foundation.Parabolic.Vec3) in Ω, ∑ i : Fin 3, f (x, s) i * (fderiv ℝ ψ x) (basisVec i) = 0

One null set for every test function, divergence form. If for each smooth compactly supported ψ supported in the open set Ω the slice divergence pairing of f vanishes for almost every time, and almost every slice of f is locally integrable on Ω, then for almost every time the slice divergence pairing vanishes for every such ψ.

theorem CKN.ae_distributional_divergence_free_of_forall_test {I : Set ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hloc : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∀ (i : Fin 3), MeasureTheory.LocallyIntegrable (fun (x : Foundation.Parabolic.Vec3) => f (x, s) i) MeasureTheory.volume) (hslice : ∀ (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, f (x, s) i * (fderiv ℝ ψ x) (basisVec i) = 0) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∀ (ψ : Foundation.Parabolic.Vec3 → ℝ), (∀ (n : ℕ), ContDiff ℝ (↑↑n) ψ) ∧ HasCompactSupport ψ → ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, f (x, s) i * (fderiv ℝ ψ x) (basisVec i) = 0

The full-space divergence statement. For almost every time the slice f(·, s) is divergence free in the sense of distributions, tested against every smooth compactly supported spatial test function. The conclusion is stated in the unfolded form used by the pressure module: it reads ∀ᵐ s, DistributionalDivergenceFree (fun x => f (x, s)).