A measurable field for the all-time local trace

The weakly continuous local L³ trace admits a jointly measurable representative that retains its uniform bound on every time slice.

theorem ESS.blowup_limit_trace_eq_source_ae_slices {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (v : ↑(Set.Icc (-(3 / 4) ^ 2) 0) → ↥(MeasureTheory.Lp CKN.Foundation.Parabolic.L2Vec3 3 (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4))))) (W : CKN.Foundation.Parabolic.Vec3 × ↑(Set.Icc (-(3 / 4) ^ 2) 0) → CKN.Foundation.Parabolic.Vec3) (hrep : ∀ (t : ↑(Set.Icc (-(3 / 4) ^ 2) 0)), (fun (x : CKN.Foundation.Parabolic.Vec3) => W (x, t)) =ᵐ[MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4))] fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.weakContL3OfLp (↑↑(v t) x)) (htrace : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-(3 / 4) ^ 2) 0), ∃ (ht : t ∈ Set.Icc (-(3 / 4) ^ 2) 0) (huSlice : MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => WithLp.toLp 2 (u (x, t))) 3 (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4)))), v ⟨t, ht⟩ = MeasureTheory.MemLp.toLp (fun (x : CKN.Foundation.Parabolic.Vec3) => WithLp.toLp 2 (u (x, t))) huSlice) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-(3 / 4) ^ 2) 0), ∃ (ht : t ∈ Set.Icc (-(3 / 4) ^ 2) 0), (fun (x : CKN.Foundation.Parabolic.Vec3) => W (x, ⟨t, ht⟩)) =ᵐ[MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4))] fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t)

The jointly measurable representative agrees with the original source field on almost every inner-ball time slice.