Jointly measurable representatives of continuous L² curves #
A continuous curve in L²(ℝ³) over a compact time interval has a jointly measurable space-time
representative whose time slices represent the curve at every time: the limit of the spatial
mollifications (prop:lps-local-strong).
theorem
ESS.LPS.lps_curve_measurable_rep
{a b : ℝ}
(hab : a ≤ b)
{L : ↑(Set.Icc a b) → ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)}
(hL : Continuous L)
:
∃ (f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
MeasureTheory.StronglyMeasurable f ∧ ∀ (t : ℝ) (ht : t ∈ Set.Icc a b),
(fun (x : CKN.Foundation.Parabolic.Vec3) => f (x, t)) =ᵐ[MeasureTheory.volume] ↑↑(L ⟨t, ht⟩)
A continuous L² curve over a closed time interval has a jointly strongly measurable
representative whose slice at every time of the interval represents the curve.