Vorticity components from a gradient field

The weak vorticity of a gradient field and its antisymmetric matrix. The antisymmetric part ∂ᵢ uₖ - ∂ₖ uᵢ of the gradient is a signed vorticity component; this is the curl input of the div–curl recovery in thm:vorticity-regularity.

def ESS.vorticityCurl (G : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (l : Fin 3) (z : CKN.Foundation.Parabolic.Vec3 × ℝ) : ℝ

The vorticity of a space-time gradient field G i j = ∂ⱼ uᵢ.

Equations

• ESS.vorticityCurl G l z = ESS.weakVorticity (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) => G i j z) z l

def ESS.vorticityAntisym (v : Fin 3 → ℝ) : Fin 3 → Fin 3 → ℝ

The antisymmetric matrix of a vector: vorticityAntisym v i k = ∑ₗ εᵢₖₗ vₗ.

Equations

• ESS.vorticityAntisym v = ![![0, v 2, -v 1], ![-v 2, 0, v 0], ![v 1, -v 0, 0]]

def ESS.vorticityEps (i k l : Fin 3) : ℝ

The coefficients of the antisymmetric matrix.

Equations

• ESS.vorticityEps i k l = ESS.vorticityAntisym (fun (m : Fin 3) => if m = l then 1 else 0) i k

theorem ESS.vorticityAntisym_curl (G : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (z : CKN.Foundation.Parabolic.Vec3 × ℝ) (i k : Fin 3) : vorticityAntisym (fun (l : Fin 3) => vorticityCurl G l z) i k = G k i z - G i k z

The antisymmetric matrix of the vorticity is the antisymmetric part of the gradient.

theorem ESS.vorticityAntisym_eq_sum (v : Fin 3 → ℝ) (i k : Fin 3) : vorticityAntisym v i k = ∑ l : Fin 3, vorticityEps i k l * v l

The antisymmetric matrix is linear in the vector.

theorem ESS.vorticityAntisym_sq_sum_le (v : Fin 3 → ℝ) : ∑ i : Fin 3, ∑ k : Fin 3, vorticityAntisym v i k ^ 2 ≤ 2 * ∑ l : Fin 3, v l ^ 2

The squared entries of the antisymmetric matrix are bounded by twice the squared norm.

theorem ESS.vorticityCurl_sq_le (G : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (z : CKN.Foundation.Parabolic.Vec3 × ℝ) (l : Fin 3) : vorticityCurl G l z ^ 2 ≤ 2 * ∑ i : Fin 3, ∑ j : Fin 3, G i j z ^ 2

The squared vorticity is bounded by four times the squared gradient.