Slice limits of strong solutions #
Componentwise L² continuity and the continuity of the pairing of a strongly
L²-continuous velocity with a test field (lem:lps-continuation).
theorem
ESS.lps_component_l2_tendsto
{E : Type}
[NormedAddCommGroup E]
{l : Filter ℝ}
{f : ℝ → CKN.Foundation.Parabolic.Vec3 → Fin 3 → E}
{f₀ : CKN.Foundation.Parabolic.Vec3 → Fin 3 → E}
(hm :
∀ᶠ (s : ℝ) in l, MeasureTheory.AEStronglyMeasurable (fun (x : CKN.Foundation.Parabolic.Vec3) => f s x - f₀ x) MeasureTheory.volume)
(h :
Filter.Tendsto
(fun (s : ℝ) =>
MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => f s x - f₀ x) 2 MeasureTheory.volume)
l (nhds 0))
(i : Fin 3)
:
Filter.Tendsto
(fun (s : ℝ) =>
MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => f s x i - f₀ x i) 2 MeasureTheory.volume)
l (nhds 0)
Componentwise L² distance is bounded by the L² distance of the vector field.
theorem
ESS.lps_vector_pairing_tendsto
{S : Set ℝ}
{t₀ : ℝ}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{φ : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3}
(hφ : ContDiff ℝ (↑⊤) φ)
(hφc : HasCompactSupport φ)
(hcont :
Filter.Tendsto
(fun (s : ℝ) =>
MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, s) - u (x, t₀)) 2 MeasureTheory.volume)
(nhdsWithin t₀ S) (nhds 0))
(hmem : ∀ s ∈ S, MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, s)) 2 MeasureTheory.volume)
(hmem₀ : MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t₀)) 2 MeasureTheory.volume)
:
The pairing of a strongly L²-continuous field with a test field is continuous.