Joint continuity of the smooth slice representatives #
lem:lps-Bochner-joint-smooth: if the slices of a space-time field form
L²-continuous curves of all-order Sobolev families, the smooth slice
representatives depend continuously on time uniformly in space, together with
every ordered derivative.
theorem
ESS.lps_sobolevNormSq_curve_tendsto
{a b : ℝ}
{Z : ℝ → List (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ}
(hfam : ∀ t ∈ Set.Icc a b, ∀ (m : ℕ), CKN.IsSobolevFamilyOn m Set.univ (Z t []) (Z t))
(hcont :
∀ (α : List (Fin 3)),
∀ t ∈ Set.Icc a b,
Filter.Tendsto (fun (s : ℝ) => MeasureTheory.eLpNorm (Z s α - Z t α) 2 MeasureTheory.volume)
(nhdsWithin t (Set.Icc a b)) (nhds 0))
(k : ℕ)
{t : ℝ}
(ht : t ∈ Set.Icc a b)
:
Filter.Tendsto
(fun (s : ℝ) =>
CKN.sobolevNormSqOn (k + 2) Set.univ fun (β : List (Fin 3)) (y : CKN.Foundation.Parabolic.Vec3) =>
Z t β y - Z s β y)
(nhdsWithin t (Set.Icc a b)) (nhds 0)
The H^{k+2} norm squared of the difference of two slice families tends to zero
with the time difference, given L² continuity of every slot
(lem:lps-Bochner-joint-smooth).
theorem
ESS.lps_smooth_rep_diff_bound
{f₁ f₂ g₁ g₂ : CKN.Foundation.Parabolic.Vec3 → ℝ}
{D₁ D₂ : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ}
(h₁ : ∀ (m : ℕ), CKN.IsSobolevFamilyOn m Set.univ f₁ D₁)
(h₂ : ∀ (m : ℕ), CKN.IsSobolevFamilyOn m Set.univ f₂ D₂)
(hg₁ : ContDiff ℝ (↑⊤) g₁)
(hg₂ : ContDiff ℝ (↑⊤) g₂)
(e₁ : g₁ =ᵐ[MeasureTheory.volume] f₁)
(e₂ : g₂ =ᵐ[MeasureTheory.volume] f₂)
(k : ℕ)
(α : List (Fin 3))
(hα : α.length ≤ k)
(x : CKN.Foundation.Parabolic.Vec3)
:
|CKN.wordDeriv α g₁ x - CKN.wordDeriv α g₂ x| ≤ lpsEmbC k * √(CKN.sobolevNormSqOn (k + 2) Set.univ fun (β : List (Fin 3)) (y : CKN.Foundation.Parabolic.Vec3) =>
D₁ β y - D₂ β y)
The difference of two smooth slice representatives is controlled in every ordered
derivative by the Sobolev distance of the slices (lem:lps-Bochner-joint-smooth).
theorem
ESS.lps_wordDeriv_rep_jointContinuousOn
{a b : ℝ}
{Z : ℝ → List (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ}
{B : ℝ → CKN.Foundation.Parabolic.Vec3 → ℝ}
(hfam : ∀ t ∈ Set.Icc a b, ∀ (m : ℕ), CKN.IsSobolevFamilyOn m Set.univ (Z t []) (Z t))
(hcont :
∀ (α : List (Fin 3)),
∀ t ∈ Set.Icc a b,
Filter.Tendsto (fun (s : ℝ) => MeasureTheory.eLpNorm (Z s α - Z t α) 2 MeasureTheory.volume)
(nhdsWithin t (Set.Icc a b)) (nhds 0))
(hBs : ∀ t ∈ Set.Icc a b, ContDiff ℝ (↑⊤) (B t) ∧ B t =ᵐ[MeasureTheory.volume] Z t [])
(α : List (Fin 3))
:
ContinuousOn (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.wordDeriv α (B z.2) z.1) (Set.univ ×ˢ Set.Icc a b)
Joint continuity in space and time of every ordered derivative of the smooth slice
representatives (lem:lps-Bochner-joint-smooth).