Vanishing of transport trilinear forms

For a weakly divergence-free field b, the transport form ∫ bⱼ (∂ⱼ fₖ gₖ + fₖ ∂ⱼ gₖ) vanishes whenever the products involved are integrable. The proof tests the weak product rule for bⱼ fₖ with cut-off mollifications of g and passes to the limit. These identities reduce the cross-testing identity to the relative energy inequality in lem:pv-serrin-uniqueness.

theorem ESS.serrin_trilinear_vanish {b f g : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {Db Df Dg : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} (hb2 : MeasureTheory.MemLp b 2 MeasureTheory.volume) (hDb2 : MeasureTheory.MemLp Db 2 MeasureTheory.volume) (hbgrad : ∀ (i : Fin 3), CKN.HasWeakGradientOn Set.univ (fun (x : CKN.Vec 3) => b x i) fun (x : CKN.Vec 3) => Db x i) (hbtr : ∀ᵐ (x : CKN.Foundation.Parabolic.Vec3), ∑ j : Fin 3, Db x j j = 0) (hf2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hDf2 : MeasureTheory.MemLp Df 2 MeasureTheory.volume) (hfgrad : ∀ (i : Fin 3), CKN.HasWeakGradientOn Set.univ (fun (x : CKN.Vec 3) => f x i) fun (x : CKN.Vec 3) => Df x i) (hg2 : MeasureTheory.MemLp g 2 MeasureTheory.volume) (hDg2 : MeasureTheory.MemLp Dg 2 MeasureTheory.volume) (hggrad : ∀ (i : Fin 3), CKN.HasWeakGradientOn Set.univ (fun (x : CKN.Vec 3) => g x i) fun (x : CKN.Vec 3) => Dg x i) {r s : ENNReal} [r.HolderTriple s 1] (hs : 1 ≤ s) (hstop : s ≠ ⊤) (hbf : ∀ (j k : Fin 3), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => b x j * f x k) 2 MeasureTheory.volume) (hbDf : ∀ (j k : Fin 3), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => b x j * Df x k j) r MeasureTheory.volume) (hg : ∀ (k : Fin 3), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => g x k) s MeasureTheory.volume) : ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : Fin 3, ∑ j : Fin 3, b x j * (Df x k j * g x k + f x k * Dg x k j) = 0

The transport trilinear form of a weakly divergence-free field vanishes.