Time regularity of the slices of the compactness limit #
Continuity in L² of a curve which represents slices at every time gives the continuity of the
slices, and weak partial derivatives of almost every slice extend to every slice when the weak
derivative is represented by a continuous curve (prop:lps-local-strong).
theorem
ESS.LPS.lps_curve_slices_tendsto
{a b : ℝ}
(hab : a < b)
{F : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
{L : ↑(Set.Icc a b) → ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)}
(hL : Continuous L)
(hrep :
∀ (t : ℝ) (ht : t ∈ Set.Icc a b),
↑↑(L ⟨t, ht⟩) =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => F (x, t))
{t : ℝ}
(ht : 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)
The slices of a function represented at every time by a continuous L² curve are continuous
in L².
theorem
ESS.LPS.lps_weak_partial_all_times
{a b : ℝ}
(hab : a < b)
(j : Fin 3)
{F G : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
{L : ↑(Set.Icc a b) → ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)}
(hL : Continuous L)
(hLG :
∀ (t : ℝ) (ht : t ∈ Set.Icc a b),
↑↑(L ⟨t, ht⟩) =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => G (x, t))
(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))
(hslice :
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), CKN.HasWeakPartialDerivOn Set.univ j (fun (x : CKN.Vec 3) => F (x, t)) fun (x : CKN.Vec 3) => G (x, t))
(t : ℝ)
:
A weak spatial derivative of almost every slice, represented by a continuous L² curve, is a
weak spatial derivative of every slice when the slices are weakly continuous.