Weak derivatives of the vorticity flux

The vorticity flux -(uⱼ ωᵢ - ωⱼ uᵢ) and its first derivative are sums of products of square-integrable fields with square-integrable weak derivatives; the product rule gives their weak derivatives (the product structure of lem:vorticity-products).

theorem ESS.vorticity_weakPartial_prodDiff {W : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} (hWo : IsOpen W) (hWb : Bornology.IsBounded W) {a b c d a' b' c' d' : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {m : Fin 3} (ha : MeasureTheory.MemLp a 2 (MeasureTheory.volume.restrict W)) (hb : MeasureTheory.MemLp b 2 (MeasureTheory.volume.restrict W)) (hc : MeasureTheory.MemLp c 2 (MeasureTheory.volume.restrict W)) (hd : MeasureTheory.MemLp d 2 (MeasureTheory.volume.restrict W)) (ha' : MeasureTheory.MemLp a' 2 (MeasureTheory.volume.restrict W)) (hb' : MeasureTheory.MemLp b' 2 (MeasureTheory.volume.restrict W)) (hc' : MeasureTheory.MemLp c' 2 (MeasureTheory.volume.restrict W)) (hd' : MeasureTheory.MemLp d' 2 (MeasureTheory.volume.restrict W)) (hda : ∀ (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, a y * CKN.spatialPartial ψ m y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, a' y * ψ y) (hdb : ∀ (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, b y * CKN.spatialPartial ψ m y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, b' y * ψ y) (hdc : ∀ (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, c y * CKN.spatialPartial ψ m y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, c' y * ψ y) (hdd : ∀ (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, d y * CKN.spatialPartial ψ m y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, d' y * ψ y) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) : ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, (a y * b y - c y * d y) * CKN.spatialPartial ψ m y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, (a' y * b y + a y * b' y - (c' y * d y + c y * d' y)) * ψ y

The weak derivative of a difference of two products.