Level sums for the interior estimates

The sums of absolute values of the vorticity, of its first and second spatial derivatives, and of the first and second spatial derivatives of the velocity, which carry the successive levels of the interior estimates in the proof of lem:aniso:annulus, with their nonnegativity and their continuity on the unit cylinder for a smooth velocity.

noncomputable def CIV.vortSum0 (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : ℝ

∑ᵢ |ωᵢ|.

Equations

• CIV.vortSum0 u z = ∑ i : Fin 3, |CIV.curlComp u i z|

noncomputable def CIV.vortSum1 (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : ℝ

∑ᵢⱼ |∂ⱼωᵢ|.

Equations

• CIV.vortSum1 u z = ∑ i : Fin 3, ∑ j : Fin 3, |CKN.spatialPartial (CIV.curlComp u i) j z|

noncomputable def CIV.vortSum2 (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : ℝ

∑ᵢⱼₗ |∂ₗ∂ⱼωᵢ|.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CIV.velSum1 (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : ℝ

∑ᵢⱼ |∂ⱼuᵢ|.

Equations

• CIV.velSum1 u z = ∑ i : Fin 3, ∑ j : Fin 3, |CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) j z|

noncomputable def CIV.velSum2 (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : ℝ

∑ᵢⱼₗ |∂ₗ∂ⱼuᵢ|.

Equations

• One or more equations did not get rendered due to their size.

theorem CIV.levelSums_nonneg (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : 0 ≤ vortSum0 u z ∧ 0 ≤ vortSum1 u z ∧ 0 ≤ vortSum2 u z ∧ 0 ≤ velSum1 u z ∧ 0 ≤ velSum2 u z

The five level sums are nonnegative.

theorem CIV.contDiffOn_curlComp_unitCylinder {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (i : Fin 3) : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => curlComp u i z) unitCylinder

The vorticity components of a velocity smooth on the unit cylinder are smooth there.

theorem CIV.continuousOn_levelSums {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) : ContinuousOn (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => vortSum0 u z) unitCylinder ∧ ContinuousOn (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => vortSum1 u z) unitCylinder ∧ ContinuousOn (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => vortSum2 u z) unitCylinder ∧ ContinuousOn (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => velSum1 u z) unitCylinder ∧ ContinuousOn (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => velSum2 u z) unitCylinder

For a velocity smooth on the unit cylinder the five level sums are continuous there.