The differentiated forced Navier–Stokes system on Ω × I

Joint smoothness of multi-index derivatives, commutation of ∂_t with ∂^α, the pressure Poisson identity Δp = div f − ∑ᵢⱼ ∂ᵢuⱼ ∂ⱼuᵢ, and the momentum equation of eq:nse:forced differentiated by ∂^α, for a classical solution on an open space-time product. These are the identities behind the one-step estimates in the proof of thm:analytic:interior.

theorem CIV.contDiffOn_spatialPartial_iterate_spaceTimeSet {g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {Ω : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} (hΩ : IsOpen Ω) (hI : IsOpen I) (hg : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => g z) (CKN.spaceTimeSet Ω I)) (j : Fin 3) (n : ℕ) : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => (fun (k : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) => CKN.spatialPartial k j)^[n] g z) (CKN.spaceTimeSet Ω I)

Iterated spatial partials of a jointly smooth field are jointly smooth.

theorem CIV.contDiffOn_multiPartial_spaceTimeSet {g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {Ω : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} (hΩ : IsOpen Ω) (hI : IsOpen I) (hg : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => g z) (CKN.spaceTimeSet Ω I)) (α : Fin 3 → ℕ) : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => multiPartial g α z) (CKN.spaceTimeSet Ω I)

Every multi-index derivative of a jointly smooth field is jointly smooth.

theorem CIV.timePartial_spatialPartial_iterate_eqOn {g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {Ω : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} (hΩ : IsOpen Ω) (hI : IsOpen I) (hg : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => g z) (CKN.spaceTimeSet Ω I)) (j : Fin 3) (n : ℕ) : Set.EqOn (CKN.timePartial ((fun (k : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) => CKN.spatialPartial k j)^[n] g)) ((fun (k : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) => CKN.spatialPartial k j)^[n] fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.timePartial g w) (CKN.spaceTimeSet Ω I)

∂_t commutes with an iterated spatial partial.

theorem CIV.timePartial_multiPartial_spaceTimeSet {g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {Ω : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} (hΩ : IsOpen Ω) (hI : IsOpen I) (hg : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => g z) (CKN.spaceTimeSet Ω I)) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ CKN.spaceTimeSet Ω I) (α : Fin 3 → ℕ) : CKN.timePartial (multiPartial g α) z = multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.timePartial g w) α z

∂_t commutes with ∂^α.

theorem CIV.spatialPartial_fin3_sum_spaceTimeSet {F : Fin 3 → CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {Ω : Set CKN.Foundation.Parabolic.Vec3} (hΩ : IsOpen Ω) (t : ℝ) (hF : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (x : CKN.Foundation.Parabolic.Vec3) => F i (x, t)) Ω) {x : CKN.Foundation.Parabolic.Vec3} (hx : x ∈ Ω) (j : Fin 3) : CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => ∑ i : Fin 3, F i w) j (x, t) = ∑ i : Fin 3, CKN.spatialPartial (F i) j (x, t)

A spatial partial of a sum of three smooth fields is the sum of the spatial partials.

theorem CIV.spatialPartial_eq_zero_of_eqOn_zero {F : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {Ω : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} (hΩ : IsOpen Ω) (hI : IsOpen I) (hF : ∀ w ∈ CKN.spaceTimeSet Ω I, F w = 0) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ CKN.spaceTimeSet Ω I) (j : Fin 3) : CKN.spatialPartial F j z = 0

A field vanishing on Ω × I has vanishing spatial partials there.

theorem CIV.timePartial_eq_zero_of_eqOn_zero {F : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {Ω : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} (hΩ : IsOpen Ω) (hI : IsOpen I) (hF : ∀ w ∈ CKN.spaceTimeSet Ω I, F w = 0) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ CKN.spaceTimeSet Ω I) : CKN.timePartial F z = 0

A field vanishing on Ω × I has vanishing time partial there.

theorem CIV.pressure_poisson_spaceTimeSet {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Ω : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} (hΩ : IsOpen Ω) (hI : IsOpen I) (hsol : IsClassicalSolutionOn u p f (CKN.spaceTimeSet Ω I)) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ CKN.spaceTimeSet Ω I) : ∑ j : Fin 3, CKN.spatialSecondPartial p j j z = ∑ i : Fin 3, CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => f w i) i z - ∑ i : Fin 3, ∑ j : Fin 3, CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w j) i z * CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) j z

The pressure Poisson identity Δp = div f − ∑ᵢⱼ ∂ᵢuⱼ ∂ⱼuᵢ for a classical solution of eq:nse:forced on Ω × I.

theorem CIV.multiPartial_sub_slice {a b : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {Ω : Set CKN.Foundation.Parabolic.Vec3} (hΩ : IsOpen Ω) (t : ℝ) (ha : ContDiffOn ℝ (↑⊤) (fun (x : CKN.Foundation.Parabolic.Vec3) => a (x, t)) Ω) (hb : ContDiffOn ℝ (↑⊤) (fun (x : CKN.Foundation.Parabolic.Vec3) => b (x, t)) Ω) (α : Fin 3 → ℕ) {x : CKN.Foundation.Parabolic.Vec3} (hx : x ∈ Ω) : multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => a w - b w) α (x, t) = multiPartial a α (x, t) - multiPartial b α (x, t)

∂^α (a - b) = ∂^α a - ∂^α b on a time slice.

theorem CIV.momentum_multiPartial_spaceTimeSet {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Ω : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} (hΩ : IsOpen Ω) (hI : IsOpen I) (hsol : IsClassicalSolutionOn u p f (CKN.spaceTimeSet Ω I)) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ CKN.spaceTimeSet Ω I) (α : Fin 3 → ℕ) (i : Fin 3) : CKN.timePartial (multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) α) z - ∑ j : Fin 3, CKN.spatialSecondPartial (multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) α) j j z = multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => f w i) α z - ∑ j : Fin 3, multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w j * CKN.spatialPartial (fun (w' : CKN.Foundation.Parabolic.ParabolicPoint) => u w' i) j w) α z - multiPartial p (α + Pi.single i 1) z

The momentum equation of eq:nse:forced differentiated by ∂^α.