Flux bounds for the vorticity energy estimate

The antisymmetric transport flux is controlled by the Euclidean sizes of the velocity and vorticity. These pointwise bounds are the algebraic input to lem:localized-vorticity-energy.

theorem ESS.vorticityFlux_component_abs_le (v z : CKN.Foundation.Parabolic.Vec3) (j i : Fin 3) : |v j * z i - z j * v i| ≤ 2 * CKN.Foundation.Parabolic.vec3EuclideanNorm v * CKN.Foundation.Parabolic.vec3EuclideanNorm z

Each coordinate of the antisymmetric vorticity flux is bounded by the product of the Euclidean sizes of its two vector arguments.

theorem ESS.vorticityFlux_pairing_abs_le (v z : CKN.Foundation.Parabolic.Vec3) (G : Fin 3 → Fin 3 → ℝ) : |∑ j : Fin 3, ∑ i : Fin 3, (v j * z i - z j * v i) * G i j| ≤ 2 * CKN.Foundation.Parabolic.vec3EuclideanNorm v * CKN.Foundation.Parabolic.vec3EuclideanNorm z * ∑ j : Fin 3, ∑ i : Fin 3, |G i j|

Pairing the flux with a matrix is bounded by the coordinatewise gradient size.

theorem ESS.vorticityFlux_pairing_l2_abs_le (v z : CKN.Foundation.Parabolic.Vec3) (G : Fin 3 → Fin 3 → ℝ) : |∑ j : Fin 3, ∑ i : Fin 3, (v j * z i - z j * v i) * G i j| ≤ 6 * CKN.Foundation.Parabolic.vec3EuclideanNorm v * CKN.Foundation.Parabolic.vec3EuclideanNorm z * √(∑ j : Fin 3, ∑ i : Fin 3, G i j ^ 2)

The flux pairing has the L² gradient bound used in the vorticity energy estimate.

theorem ESS.vorticityMatrixPairing_abs_le (F G : Fin 3 → Fin 3 → ℝ) : |∑ j : Fin 3, ∑ i : Fin 3, F j i * G i j| ≤ √(∑ j : Fin 3, ∑ i : Fin 3, F j i ^ 2) * √(∑ j : Fin 3, ∑ i : Fin 3, G i j ^ 2)

Cauchy--Schwarz for the matrix forcing term in the weak vorticity energy identity.

theorem ESS.vorticityFluxAndMatrixPairing_halfDissipation (M : ℝ) (v z : CKN.Foundation.Parabolic.Vec3) (F G : Fin 3 → Fin 3 → ℝ) (hM : 0 ≤ M) (hv : CKN.Foundation.Parabolic.vec3EuclideanNorm v ≤ M) : |∑ j : Fin 3, ∑ i : Fin 3, (v j * z i - z j * v i) * G i j| + |∑ j : Fin 3, ∑ i : Fin 3, F j i * G i j| ≤ 1 / 2 * ∑ j : Fin 3, ∑ i : Fin 3, G i j ^ 2 + 36 * M ^ 2 * CKN.Foundation.Parabolic.vec3EuclideanNorm z ^ 2 + ∑ j : Fin 3, ∑ i : Fin 3, F j i ^ 2

The transport and matrix terms use at most half of the gradient dissipation after choosing the Young parameters needed for the smooth energy estimate in lem:localized-vorticity-energy.

theorem ESS.vorticityVectorPairing_young (g z : CKN.Foundation.Parabolic.Vec3) : |∑ i : Fin 3, g i * z i| ≤ 1 / 2 * ∑ i : Fin 3, g i ^ 2 + 1 / 2 * ∑ i : Fin 3, z i ^ 2

A finite-dimensional Cauchy--Young bound for the zero-order forcing in the smooth vorticity energy calculation.