The momentum equation for concatenated solutions

A Leray–Hopf solution on (0, T) followed after time s ≤ T by a strong solution with the same slice at s satisfies the divergence-free weak momentum equation across s, since the boundary terms at s cancel (lem:lps-continuation).

theorem ESS.lps_test_partials_zero {a s : ℝ} {ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3} (hψ : ψ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a s)) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : s ≤ z.2) : (∀ (i : Fin 3), CKN.timePartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => ψ y i) z = 0) ∧ ∀ (i j : Fin 3), CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => ψ y i) j z = 0

A test field supported before s has vanishing derivatives from time s on.

theorem ESS.lps_lh_equation_restrict {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) (hsT : s ≤ T) {φ : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3} (hφ : φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo 0 s)) (hdiv : ∀ (z : CKN.Foundation.Parabolic.ParabolicPoint), ∑ i : Fin 3, CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) i z = 0) : ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 s), lpsEqIntegrand u Du (fun (x : CKN.Foundation.Parabolic.ParabolicPoint) => 0) φ z = 0

The divergence-free weak equation of a Leray–Hopf solution for a test field supported before s ≤ T, over the slab (0, s).

theorem ESS.lps_lh_memLp_slab {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) : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))) ∧ MeasureTheory.MemLp Du 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))

A Leray–Hopf solution is in L²(0,T; L²) and its almost every slice has uniformly bounded L² norm.

theorem ESS.lps_lh_slice_bound {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) (hsT : s ≤ T) : ∃ (M : ℝ), ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 s), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume ∧ (MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume).toReal ≤ M

Almost every slice of a Leray–Hopf solution on (0, s) is square integrable with a uniform bound.

theorem ESS.lps_concat_equation {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) (φ : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) : φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo 0 s') → (∀ (z : CKN.Foundation.Parabolic.ParabolicPoint), ∑ i : Fin 3, CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) i z = 0) → ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 s'), -∑ i : Fin 3, lpsGlue s u W z i * CKN.timePartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) z - ∑ i : Fin 3, ∑ j : Fin 3, lpsGlue s u W z i * lpsGlue s u W z j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z + ∑ i : Fin 3, ∑ j : Fin 3, lpsGlue s Du DW z i j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z = 0

The divergence-free weak momentum equation holds across the junction of a Leray–Hopf solution and a strong solution with the same slice (lem:lps-continuation).