Weak vorticity

The vorticity associated to the explicit weak gradient of a velocity field.

def ESS.weakVorticity (Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3

The weak vorticity determined by the velocity gradient convention Du z i j = ∂ⱼ uᵢ (manuscript thm:vorticity-regularity).

Equations

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

def ESS.vorticityFlux (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) (j i : Fin 3) : ℝ

The divergence-form flux in the weak vorticity equation thm:vorticity-regularity.

Equations

• ESS.vorticityFlux u Du z j i = u z j * ESS.weakVorticity Du z i - ESS.weakVorticity Du z j * u z i

@[simp]

theorem ESS.weakVorticity_zero (Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : weakVorticity Du z 0 = Du z 2 1 - Du z 1 2

@[simp]

theorem ESS.weakVorticity_one (Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : weakVorticity Du z 1 = Du z 0 2 - Du z 2 0

@[simp]

theorem ESS.weakVorticity_two (Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : weakVorticity Du z 2 = Du z 1 0 - Du z 0 1