Identification of a continuous curve with weakly continuous slices #
A continuous L² curve which represents a family of L² slices for almost every time represents
it at every time when the family is weakly continuous (prop:lps-local-strong).
theorem
ESS.LPS.lps_eqOn_Icc_of_ae_eq
{a b : ℝ}
(hab : a < b)
{f g : ℝ → ℝ}
(hf : ContinuousOn f (Set.Icc a b))
(hg : ContinuousOn g (Set.Icc a b))
(h : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), f s = g s)
:
Two continuous functions on a closed interval that agree almost everywhere on its interior agree everywhere.
theorem
ESS.LPS.lps_curve_eq_of_weak_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)
(hFweak :
∀ (w : CKN.Foundation.Parabolic.Vec3 → ℝ),
MeasureTheory.MemLp w 2 MeasureTheory.volume →
ContinuousOn (fun (t : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), F (x, t) * w x) (Set.Icc a b))
(t : ℝ)
(ht : t ∈ Set.Icc a b)
:
↑↑(L ⟨t, ht⟩) =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => F (x, t)
A continuous L² curve representing a weakly continuous family of L² slices almost
everywhere represents it everywhere.