Comparing a strong continuation with a Leray–Hopf solution #
A strong solution started, from a time of energy equality, at the slice of a
Leray–Hopf solution with finite Serrin norm coincides with it, by
uniqueness of Leray–Hopf solutions applied to the concatenation
(lem:lps-continuation).
theorem
ESS.lps_serrin_restrict
{T σ : ℝ}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hσT : σ ≤ T)
(hSerrin :
(∃ (s : ℝ),
3 < s ∧ ∫⁻ (t : ℝ) in Set.Ioo 0 T, (∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) ^ s) ^ (2 * s / (s - 3) / s) < ⊤) ∨ ∫⁻ (t : ℝ) in Set.Ioo 0 T, essSup
(fun (x : CKN.Foundation.Parabolic.Vec3) =>
ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t))))
MeasureTheory.volume ^ 2 < ⊤)
:
(∃ (s : ℝ),
3 < s ∧ ∫⁻ (t : ℝ) in Set.Ioo 0 σ, (∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) ^ s) ^ (2 * s / (s - 3) / s) < ⊤) ∨ ∫⁻ (t : ℝ) in Set.Ioo 0 σ, essSup
(fun (x : CKN.Foundation.Parabolic.Vec3) =>
ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t))))
MeasureTheory.volume ^ 2 < ⊤
The Serrin hypotheses of thm:lps are inherited by shorter time intervals.
theorem
ESS.lps_continuation_compare
{T s s' : ℝ}
{a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{W : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{DW : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{pW : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
(hLH : CKN.IsLerayHopfSolution T a u Du)
(hSerrin :
(∃ (s : ℝ),
3 < s ∧ ∫⁻ (t : ℝ) in Set.Ioo 0 T, (∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) ^ s) ^ (2 * s / (s - 3) / s) < ⊤) ∨ ∫⁻ (t : ℝ) in Set.Ioo 0 T, essSup
(fun (x : CKN.Foundation.Parabolic.Vec3) =>
ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t))))
MeasureTheory.volume ^ 2 < ⊤)
(hs0 : 0 < s)
(hsT : s ≤ T)
(hW : IsLpsStrongSolution s s' W DW pW)
(hweakEq :
∀ (w : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3),
MeasureTheory.MemLp w 2 MeasureTheory.volume →
∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, W (x, s) i * w x i = ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, u (x, s) i * w x i)
(hEnergy :
(ENNReal.ofReal (1 / 2) * ∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (W (x, s))) ^ 2) + ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 s), ENNReal.ofReal (CKN.spatialGradientSq u Du z) = ENNReal.ofReal (1 / 2) * ∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (a x)) ^ 2)
:
W =ᵐ[MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo s (min s' T)))] u
A strong solution started from a slice of a Leray–Hopf solution with finite
Serrin norm, at a time of energy equality, agrees with it on the common time
interval (lem:lps-continuation).