Continuous curves coincide with continuous slices #
A continuous L² curve that represents a slice family for almost every time
represents it at every time, whenever the slice family itself is continuous in
L² (prop:lps-local-strong).
theorem
ESS.LPS.lps_lp_norm_sq_eq
{L : ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)}
{f : CKN.Foundation.Parabolic.Vec3 → ℝ}
(h : ↑↑L =ᵐ[MeasureTheory.volume] f)
(hf : MeasureTheory.MemLp f 2 MeasureTheory.volume)
:
The squared norm of an L² class is the integral of the square of any
representative.
theorem
ESS.LPS.lps_curve_eq_of_continuous
{a b : ℝ}
(hab : a < b)
{F : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
{L : ↑(Set.Icc a b) → ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)}
(hL : Continuous L)
(hLF :
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), ∀ (hs : s ∈ Set.Icc a b),
↑↑(L ⟨s, hs⟩) =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => F (x, s))
(hFmem :
∀ t ∈ Set.Icc a b, MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => F (x, t)) 2 MeasureTheory.volume)
(hFc :
∀ t ∈ Set.Icc a b,
Filter.Tendsto
(fun (s : ℝ) =>
MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => F (x, s) - F (x, t)) 2 MeasureTheory.volume)
(nhdsWithin t (Set.Icc a b)) (nhds 0))
(t : ℝ)
(ht : t ∈ Set.Icc a b)
:
↑↑(L ⟨t, ht⟩) =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => F (x, t)
A continuous curve representing a continuous slice family almost everywhere represents it everywhere.