The energy equality at the restart time #
The energy equality of a Leray–Hopf solution at a good time, in the extended-real
form of the Leray–Hopf energy inequality, and its propagation along a strong
continuation (lem:lps-continuation).
theorem
ESS.lps_lh_energy_ennreal
{T 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)
(ht₀ : t₀ ∈ Set.Ioo 0 T)
(hm : MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t₀)) 2 MeasureTheory.volume)
(hreal :
(∫ (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)
:
(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
The real form of the energy equality at a good time, as the extended-real form of the Leray–Hopf energy inequality with equality.
theorem
ESS.lps_restart_energy
{T t₀ 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}
{U W : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{DU : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
(hLH : CKN.IsLerayHopfSolution T a u Du)
(hU : IsLpsStrongSolution t₀ t₁ U DU p)
(ht₀ : 0 < t₀)
(ht₁ : t₁ ≤ T)
(hae : U =ᵐ[MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ t₁))] u)
(hU0 :
(fun (x : CKN.Foundation.Parabolic.Vec3) => U (x, t₀)) =ᵐ[MeasureTheory.volume]
fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, 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)
(hW0 :
(fun (x : CKN.Foundation.Parabolic.Vec3) => W (x, t₁)) =ᵐ[MeasureTheory.volume]
fun (x : CKN.Foundation.Parabolic.Vec3) => U (x, t₁))
:
(ENNReal.ofReal (1 / 2) * ∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (W (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
The energy equality of a Leray–Hopf solution at the end time of a strong
solution that agrees with it, in the extended-real form
(lem:lps-continuation).