Endpoint data for strong solutions #
The closed-interval strong-solution class supplies an H¹ ∩ J endpoint
slice, which can be used as data for a translated local strong solution
(lem:lps-continuation).
theorem
ESS.lps_strong_solution_endpoint_trace
{t₀ t₁ : ℝ}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
(hU : IsLpsStrongSolution t₀ t₁ u Du p)
:
IsLpsGoodTime u Du t₁ ∧ Filter.Tendsto
(fun (s : ℝ) =>
MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, s) - u (x, t₁)) 2 MeasureTheory.volume)
(nhdsWithin t₁ (Set.Icc t₀ t₁)) (nhds 0) ∧ Filter.Tendsto
(fun (s : ℝ) =>
MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => Du (x, s) - Du (x, t₁)) 2
MeasureTheory.volume)
(nhdsWithin t₁ (Set.Icc t₀ t₁)) (nhds 0)
The terminal slice of a strong solution is solenoidal and belongs to
H¹ with its specified weak gradient (lem:lps-continuation).
theorem
ESS.lps_strong_solution_endpoint_good_time
{t₀ t₁ : ℝ}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
(hU : IsLpsStrongSolution t₀ t₁ u Du p)
:
IsLpsGoodTime u Du t₁
The terminal slice of a strong solution is solenoidal and belongs to
H¹ with its specified weak gradient (lem:lps-continuation).