A measurable weak gradient on a countable union of time windows

The pressure gradient in paper/ckn.tex, Section sec:pressure, is first constructed on spatial slices. Selection on integrable time windows and countable pasting give a jointly measurable representative on their union. The representative remains locally integrable and a weak derivative on almost every spatial slice, so uniqueness identifies it with every derivative on an open subdomain of the carrier.

theorem CKN.exists_measurable_weakGradient_on_time_union {B U : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {p : Foundation.Parabolic.ParabolicPoint → ℝ} (hB : IsOpen B) (hU : IsOpen U) (hUc : IsCompact (closure U)) (hUB : closure U ⊆ B) {J : ℕ → Set ℝ} (hJ : ∀ (n : ℕ), MeasurableSet (J n)) (hJI : ⋃ (n : ℕ), J n = I) (hp : ∀ (n : ℕ), MeasureTheory.IntegrableOn p (B ×ˢ J n) MeasureTheory.volume) (hslice : ∀ (k : Fin 3), ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∃ (g : Foundation.Parabolic.Vec3 → ℝ), MeasureTheory.LocallyIntegrableOn g B MeasureTheory.volume ∧ HasWeakPartialDerivOn B k (fun (x : Vec 3) => p (x, s)) g) : ∃ (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3), Measurable Dp ∧ ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∀ (k : Fin 3), MeasureTheory.LocallyIntegrableOn (fun (x : Foundation.Parabolic.Vec3) => Dp (x, s) k) U MeasureTheory.volume ∧ (HasWeakPartialDerivOn U k (fun (x : Vec 3) => p (x, s)) fun (x : Vec 3) => Dp (x, s) k) ∧ ∀ (W : Set Foundation.Parabolic.Vec3), IsOpen W → W ⊆ U → ∀ (g : Foundation.Parabolic.Vec3 → ℝ), MeasureTheory.LocallyIntegrableOn g W MeasureTheory.volume → HasWeakPartialDerivOn W k (fun (x : Vec 3) => p (x, s)) g → (fun (x : Foundation.Parabolic.Vec3) => Dp (x, s) k) =ᵐ[MeasureTheory.volume.restrict W] g

Slice gradients on a countable union of integrable time windows have a jointly measurable representative on every relatively compact open inner carrier. All coordinates and all open subdomains share one exceptional time set.