Convection pairing for weak vorticity

The weak product rule and the zero gradient trace reduce the convection term to the cross product of velocity and vorticity.

theorem ESS.suitableWeakConvectionPairingDivergenceFree {U : Set CKN.Foundation.Parabolic.Vec3} (hU : IsOpen U) (hUfinite : (MeasureTheory.volume.restrict U) Set.univ < ⊤) {v : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {Dv : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} (hv : ∀ (i : Fin 3), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => v x i) 2 (MeasureTheory.volume.restrict U)) (hDv : MeasureTheory.MemLp Dv 2 (MeasureTheory.volume.restrict U)) (hweak : ∀ (i : Fin 3), CKN.HasWeakGradientOn U (fun (x : CKN.Vec 3) => v x i) fun (x : CKN.Vec 3) => Dv x i) (htrace : (fun (x : CKN.Foundation.Parabolic.Vec3) => ∑ i : Fin 3, Dv x i i) =ᵐ[MeasureTheory.volume.restrict U] 0) {φ : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hφ : ∀ (i : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => φ x i) (hφc : ∀ (i : Fin 3), HasCompactSupport fun (x : CKN.Foundation.Parabolic.Vec3) => φ x i) (hφU : ∀ (i : Fin 3), (tsupport fun (x : CKN.Foundation.Parabolic.Vec3) => φ x i) ⊆ U) (hdivφ : ∀ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => φ y i) i x = 0) : ∑ i : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3) in U, ∑ j : Fin 3, v x i * v x j * CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => φ y i) j x = ∑ i : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3) in U, spatialCross (v x) (spatialWeakVorticity Dv x) i * φ x i

The nonlinear term tested against a divergence-free field is the pairing with the cross product of velocity and weak vorticity (manuscript lem:vorticity-weak-eq).