Spatial derivatives of the vorticity equation in divergence form

If ∂ₜw − Δw = ∑ₘ ∂ₘ Yₘ on the unit cylinder with smooth w and Y, then each spatial derivative satisfies ∂ₜ(∂ⱼw) − Δ(∂ⱼw) = ∑ₘ ∂ₘ(∂ⱼYₘ). Applied to the divergence form of the vorticity equation, this gives the equations of the first and second spatial derivatives of the vorticity used at the successive levels of the interior estimates in the proof of lem:aniso:annulus.

theorem CIV.isOpen_vec3Ball_zero_one : IsOpen (CKN.Foundation.Parabolic.vec3Ball 0 1)

theorem CIV.spatialPartial_fin3_sum_unitCylinder {G : Fin 3 → CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hG : ∀ (m : Fin 3), ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => G m z) unitCylinder) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ unitCylinder) (j : Fin 3) : CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => ∑ m : Fin 3, G m w) j z = ∑ m : Fin 3, CKN.spatialPartial (G m) j z

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

theorem CIV.heat_divergence_equation_spatialPartial {w : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {Y : Fin 3 → CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hw : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => w z) unitCylinder) (hY : ∀ (m : Fin 3), ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => Y m z) unitCylinder) (heq : ∀ z ∈ unitCylinder, CKN.timePartial w z - ∑ m : Fin 3, CKN.spatialSecondPartial w m m z = ∑ m : Fin 3, CKN.spatialPartial (Y m) m z) (j : Fin 3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : z ∈ unitCylinder → CKN.timePartial (fun (v : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial w j v) z - ∑ m : Fin 3, CKN.spatialSecondPartial (fun (v : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial w j v) m m z = ∑ m : Fin 3, CKN.spatialPartial (fun (v : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial (Y m) j v) m z

Differentiating a heat equation in divergence form in a spatial direction.

theorem CIV.contDiffOn_serrinVortFlux {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hcl : IsClassicalSolutionOn u p f unitCylinder) (i m : Fin 3) : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => serrinVortFlux u f i m z) unitCylinder

The vorticity components, and the fluxes of the divergence form, are smooth on the unit cylinder for a classical solution.

theorem CIV.vorticity_first_derivative_equation {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hcl : IsClassicalSolutionOn u p f unitCylinder) (z : CKN.Foundation.Parabolic.ParabolicPoint) : z ∈ unitCylinder → ∀ (i j : Fin 3), CKN.timePartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial (curlComp u i) j w) z - ∑ m : Fin 3, CKN.spatialSecondPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial (curlComp u i) j w) m m z = ∑ m : Fin 3, CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial (serrinVortFlux u f i m) j w) m z

The equation of the first spatial derivatives of the vorticity.

theorem CIV.vorticity_second_derivative_equation {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hcl : IsClassicalSolutionOn u p f unitCylinder) (z : CKN.Foundation.Parabolic.ParabolicPoint) : z ∈ unitCylinder → ∀ (i j l : Fin 3), CKN.timePartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial (fun (w' : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial (curlComp u i) j w') l w) z - ∑ m : Fin 3, CKN.spatialSecondPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial (fun (w' : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial (curlComp u i) j w') l w) m m z = ∑ m : Fin 3, CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial (fun (w' : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial (serrinVortFlux u f i m) j w') l w) m z

The equation of the second spatial derivatives of the vorticity.