The strong equation with its time derivative, and solenoidality

For a strong solution in the class of prop:lps-local-strong, integrating the term -u · ∂ₜφ of the weak momentum equation by parts in time gives the equation with the weak time derivative ∂ₜu tested against φ, and every time slice being weakly solenoidal gives ∑ᵢ ∂ᵢuᵢ = 0 almost everywhere on the slab. Both are inputs of the difference-quotient argument of prop:lps-smoothing.

theorem ESS.LPS.lps_weakEquation_integrand_integrable {I J : Set ℝ} {A : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {F : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → ℝ} {G : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {q : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hA : MeasureTheory.MemLp A 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ I))) (hF : ∀ (i j : Fin 3), MeasureTheory.Integrable (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => F z i j) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ I))) (hG : MeasureTheory.MemLp G 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ I))) (hq : MeasureTheory.MemLp q 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ I))) {φ : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hφ : φ ∈ CKN.spaceTimeTestFunction Set.univ J) : MeasureTheory.Integrable (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => ∑ i : Fin 3, A z i * φ z i - ∑ i : Fin 3, ∑ j : Fin 3, F z i j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z + ∑ i : Fin 3, ∑ j : Fin 3, G z i j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z - q z * ∑ i : Fin 3, CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) i z) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ I))

Integrability, against a space-time test field, of the integrand of the weak momentum equation written with a time-derivative field A, a flux F, a gradient field G and a pressure q (prop:lps-smoothing). Only F is merely integrable.

theorem ESS.LPS.lps_strong_solution_equation_Dtu {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 → ℝ} {D2u : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} {Dtu : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hsol : IsLpsStrongSolution t₀ T u Du p) (hderiv : CKN.HasSpaceTimeWeakDerivs Set.univ (Set.Ioo t₀ T) u Du D2u Dtu) (hDtu : MeasureTheory.MemLp Dtu 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T)))) (φ : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) : φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo t₀ T) → ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T), ∑ i : Fin 3, Dtu z i * φ z i - ∑ i : Fin 3, ∑ j : Fin 3, u z i * u z j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z + ∑ i : Fin 3, ∑ j : Fin 3, Du z i j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z - p z * ∑ i : Fin 3, CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) i z = 0

The weak momentum equation of a strong solution, with the term -u · ∂ₜφ integrated by parts in time against a weak time derivative Dtu of u (prop:lps-smoothing).

theorem ESS.LPS.lps_strong_solution_div_free {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 → ℝ} (hsol : IsLpsStrongSolution t₀ T u Du p) : ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T)), ∑ i : Fin 3, Du z i i = 0

The gradient of a strong solution is trace free almost everywhere on the slab: every time slice lies in J (prop:lps-local-strong, used in prop:lps-smoothing).