Commutator L2 Sq Nonneg

Supporting results for the Constantin–Ignatova–Vicol axisymmetric regularity theorem.

theorem CIV.commutatorL2Sq_nonneg {m : ℕ} (ε Rb : ℝ) (B : CKN.Vec m × ℝ → CKN.Vec m) (divB q : CKN.Vec m × ℝ → ℝ) (s : ℝ) : 0 ≤ commutatorL2Sq m ε Rb B divB q s

The squared L² mass of the DiPerna–Lions commutator on a ball is nonnegative.