Jointly measurable representatives of global slice derivatives

Spatial mollification constructs a representative from joint measurability and local integrability of almost every slice. No time-integrability bound on the derivative is needed for this selection.

theorem CKN.exists_measurable_global_slice_derivative (k : Fin 3) {p : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hp : Measurable p) (hploc : ∀ᵐ (t : ℝ), MeasureTheory.LocallyIntegrable (fun (x : Foundation.Parabolic.Vec3) => p (x, t)) MeasureTheory.volume) (hslice : ∀ᵐ (t : ℝ), ∃ (g : Foundation.Parabolic.Vec3 → ℝ), MeasureTheory.LocallyIntegrable g MeasureTheory.volume ∧ HasWeakPartialDerivOn Set.univ k (fun (x : Vec 3) => p (x, t)) g) : ∃ (D : Foundation.Parabolic.Vec3 × ℝ → ℝ), Measurable D ∧ ∀ᵐ (t : ℝ), ∀ (g : Foundation.Parabolic.Vec3 → ℝ), MeasureTheory.LocallyIntegrable g MeasureTheory.volume → HasWeakPartialDerivOn Set.univ k (fun (x : Vec 3) => p (x, t)) g → (fun (x : Foundation.Parabolic.Vec3) => D (x, t)) =ᵐ[MeasureTheory.volume] g

Global slice derivatives have a jointly measurable representative, uniquely identified with every locally integrable weak derivative on each good slice.