Concatenating a Leray–Hopf solution with a strong solution

A Leray–Hopf solution on (0, T), followed after a time s ≤ T at which it satisfies the energy equality by a strong solution with the same slice at s, is a Leray–Hopf solution on (0, s') (lem:lps-continuation). This lets a strong continuation be compared with the original solution through uniqueness of Leray–Hopf solutions.

noncomputable def ESS.lpsCat {α : Type} (b : ℝ) (f g : CKN.Foundation.Parabolic.ParabolicPoint → α) (z : CKN.Foundation.Parabolic.ParabolicPoint) : α

The field equal to f strictly before time b and to g from time b on.

Equations

• ESS.lpsCat b f g z = if z.2 < b then f z else g z

theorem ESS.lpsCat_of_lt {α : Type} {b : ℝ} {f g : CKN.Foundation.Parabolic.ParabolicPoint → α} {z : CKN.Foundation.Parabolic.ParabolicPoint} (h : z.2 < b) : lpsCat b f g z = f z

theorem ESS.lpsCat_of_ge {α : Type} {b : ℝ} {f g : CKN.Foundation.Parabolic.ParabolicPoint → α} {z : CKN.Foundation.Parabolic.ParabolicPoint} (h : b ≤ z.2) : lpsCat b f g z = g z

theorem ESS.lpsCat_ae_eq_glue {α : Type} (b : ℝ) (f g : CKN.Foundation.Parabolic.ParabolicPoint → α) : ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint), lpsCat b f g z = lpsGlue b f g z

The two ways of gluing differ only on the null slice at the gluing time.

theorem ESS.lps_leray_hopf_concat {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) (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) : CKN.IsLerayHopfSolution s' a (lpsCat s u W) (lpsCat s Du DW)

Concatenation of a Leray–Hopf solution with a strong continuation from a time of energy equality (lem:lps-continuation).