Finite-energy weak solutions with a pressure

The comparison argument of lem:pv-serrin-uniqueness uses a solution only through its energy class, its weak gradient, its divergence condition, a momentum identity with a pressure in L^{5/3}, the continuity of its pairings with smooth compactly supported fields, and its initial pairings. This file names that class; Leray–Hopf solutions and the short-time solution of prop:pv-local-solution both belong to it.

structure ESS.IsSerrinWeakSolution (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) (p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) : Prop

A finite-energy weak solution of the Navier–Stokes equations on ℝ³ × (0, T) with pressure p and datum a, in the class used by the weak–strong comparison lem:pv-serrin-uniqueness.

• pos : 0 < T
• datum : MeasureTheory.MemLp a 2 MeasureTheory.volume
• meas_u : MeasureTheory.AEStronglyMeasurable u (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))
• meas_Du : MeasureTheory.AEStronglyMeasurable Du (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))
• slice_bound : essSup (fun (s : ℝ) => ∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ‖u (x, s)‖ₑ ^ 2) (MeasureTheory.volume.restrict (Set.Ioo 0 T)) < ⊤
• energy : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 T), ‖u z‖ₑ ^ 2 + ‖Du z‖ₑ ^ 2 < ⊤
• weak_grad : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), ∀ (i : Fin 3), CKN.HasWeakGradientOn Set.univ (fun (x : CKN.Vec 3) => u (x, s) i) fun (x : CKN.Vec 3) => Du (x, s) i
• div_free : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), ∀ (ψ : CKN.WeakTestFunction Set.univ), ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, u (x, s) i * ψ.partialDeriv i x = 0
• pressure : MeasureTheory.MemLp p (ENNReal.ofReal (5 / 3)) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))
• momentum (φ : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) : φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo 0 T) → ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 T), -∑ i : Fin 3, u z i * CKN.timePartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) z - ∑ 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 - ∑ i : Fin 3, 0 z i * φ z i = 0
• weak_cont (ψ : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) : ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ContinuousOn (fun (t : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, u (x, t) i * ψ x i) (Set.Icc 0 T)
• initial (ψ : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) : ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, u (x, 0) i * ψ x i = ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, a x i * ψ x i