Representatives with pointwise spatial slice bounds

A jointly measurable field with an almost-everywhere spatial bound can be changed on a null set to obey that bound at every spatial point on almost every time slice. This preserves its value on the prescribed carrier.

theorem CKN.Core.Step4.exists_measurable_spatially_bounded_representative {H : Foundation.Parabolic.ParabolicPoint → ℝ} (hH : Measurable H) {M : ℝ → ENNReal} (hM : AEMeasurable M MeasureTheory.volume) {S : Set Foundation.Parabolic.ParabolicPoint} (hS : MeasurableSet S) (hbound : ∀ᵐ (s : ℝ) (x : Foundation.Parabolic.Vec3), (x, s) ∈ S → ‖H (x, s)‖ₑ ≤ M s) : ∃ (H' : Foundation.Parabolic.ParabolicPoint → ℝ), Measurable H' ∧ H' =ᵐ[MeasureTheory.volume.restrict S] H ∧ ∀ᵐ (s : ℝ), ∀ (x : Foundation.Parabolic.Vec3), ‖H' (x, s)‖ₑ ≤ M s

A measurable representative can satisfy a temporal bound at every spatial point, while remaining almost everywhere equal to the original field on its measurable carrier.