Continuation of a Leray–Hopf solution by strong solutions #
lem:lps-continuation: a Leray–Hopf solution of finite Serrin norm agrees, from a
good time of energy equality up to its final time and beyond, with a strong
solution. The strong solutions are built by repeated use of the local strong
existence theorem, whose lifespan is bounded below through the H¹ estimate, and
are identified with the Leray–Hopf solution by uniqueness.
theorem
ESS.lps_continuation_of_local
(hLocal :
∃ (c : ℝ),
0 < c ∧ ∀ (t : ℝ) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3)
(Db : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3),
IsLpsGoodTime (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => b z.1)
(fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i : Fin 3) => Db z.1 i) t →
∃ (τ : ℝ),
0 < τ ∧ c * (1 + √(∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, b x i ^ 2 + ∑ i : Fin 3, ∑ j : Fin 3, Db x i j ^ 2)).rpow
(-4) ≤ τ ∧ ∃ (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 → ℝ),
IsLpsStrongSolution t (t + τ) W DW pW ∧ (fun (x : CKN.Foundation.Parabolic.Vec3) => W (x, t)) =ᵐ[MeasureTheory.volume] b)
{T : ℝ}
{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}
(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 < ⊤)
{t₀ : ℝ}
(ht₀ : t₀ ∈ Set.Ioo 0 T)
(hGood : IsLpsGoodTime u Du t₀)
(hEq₀ :
(∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : Fin 3, u (x, t₀) k * u (x, t₀) k) - ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : Fin 3, a x k * a x k = -2 * ∫ (q : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t₀), ∑ k : Fin 3, ∑ j : Fin 3, Du q k j * Du q k j)
:
∃ (t₁ : ℝ),
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 → ℝ),
IsLpsStrongSolution t₀ t₁ U DU p ∧ ((fun (x : CKN.Foundation.Parabolic.Vec3) => U (x, t₀)) =ᵐ[MeasureTheory.volume]
fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t₀)) ∧ U =ᵐ[MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T))] u
A finite-Serrin-norm Leray–Hopf solution on (0, T) coincides, from a good time
t₀ of energy equality, with a strong solution on [t₀, t₁] for some t₁ > T
(lem:lps-continuation). The hypothesis hLocal is the local strong existence
theorem prop:lps-local-strong, in the form used here.
theorem
ESS.lps_continuation
{T : ℝ}
{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}
(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 < ⊤)
{t₀ : ℝ}
(ht₀ : t₀ ∈ Set.Ioo 0 T)
(hGood : IsLpsGoodTime u Du t₀)
(hEq₀ :
(∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : Fin 3, u (x, t₀) k * u (x, t₀) k) - ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : Fin 3, a x k * a x k = -2 * ∫ (q : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t₀), ∑ k : Fin 3, ∑ j : Fin 3, Du q k j * Du q k j)
:
∃ (t₁ : ℝ),
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 → ℝ),
IsLpsStrongSolution t₀ t₁ U DU p ∧ ((fun (x : CKN.Foundation.Parabolic.Vec3) => U (x, t₀)) =ᵐ[MeasureTheory.volume]
fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t₀)) ∧ U =ᵐ[MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T))] u
A finite-Serrin-norm Leray–Hopf solution on (0, T) coincides, from a good time
t₀ of energy equality, with a strong solution on [t₀, t₁] for some t₁ > T
(lem:lps-continuation).