One step of the continuation #
From a strong solution agreeing with a Leray–Hopf solution on (t₀, t₁), the local
strong existence theorem started at its terminal slice, glued to it, gives a strong
solution agreeing with the Leray–Hopf solution on a longer interval, whose length
increases by a lower bound depending only on the H¹ norm of the slice
(lem:lps-continuation).
theorem
ESS.lps_continuation_step
{c : ℝ}
(hc : 0 ≤ c)
(hLocal :
∀ (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 t₀ t₁ 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}
(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 < ⊤)
(ht₀ : 0 < t₀)
(ht₁ : 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)
(hU0 :
(fun (x : CKN.Foundation.Parabolic.Vec3) => U (x, t₀)) =ᵐ[MeasureTheory.volume]
fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t₀))
(hae : U =ᵐ[MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ t₁))] u)
(hEq₀ :
(ENNReal.ofReal (1 / 2) * ∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t₀))) ^ 2) + ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t₀), 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)
(hS :
∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, U (x, t₁) i ^ 2 + ∑ i : Fin 3, ∑ j : Fin 3, DU (x, t₁) i j ^ 2 ≤ S)
:
∃ (t₁' : ℝ),
t₁ + c * (1 + √S).rpow (-4) ≤ 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' ∧ (∀ (x : CKN.Foundation.Parabolic.Vec3), U' (x, t₀) = U (x, t₀)) ∧ (∀ (x : CKN.Foundation.Parabolic.Vec3), DU' (x, t₀) = DU (x, t₀)) ∧ U' =ᵐ[MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ (min t₁' T)))] u
One continuation step past a terminal time t₁ ≤ T of a strong solution that agrees
with a Leray–Hopf solution of finite Serrin norm (lem:lps-continuation).
theorem
ESS.lps_continuation_base
{c : ℝ}
(hc : 0 ≤ c)
(hLocal :
∀ (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 t₀ 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}
(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 < ⊤)
(ht₀ : 0 < t₀)
(ht₀T : t₀ ≤ T)
(hGood : IsLpsGoodTime u Du t₀)
(hEq₀ :
(ENNReal.ofReal (1 / 2) * ∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t₀))) ^ 2) + ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t₀), 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)
(hS :
∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, u (x, t₀) i ^ 2 + ∑ i : Fin 3, ∑ j : Fin 3, Du (x, t₀) i j ^ 2 ≤ S)
:
∃ (t₁ : ℝ),
t₀ + c * (1 + √S).rpow (-4) ≤ 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₀)) ∧ ((fun (x : CKN.Foundation.Parabolic.Vec3) => DU (x, t₀)) =ᵐ[MeasureTheory.volume]
fun (x : CKN.Foundation.Parabolic.Vec3) => Du (x, t₀)) ∧ U =ᵐ[MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ (min t₁ T)))] u
The first continuation step, from a good time t₀ ≤ T of the Leray–Hopf solution at
which the energy equality holds (lem:lps-continuation).