Grad Pair

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

noncomputable def CIV.gradPair (m : ℕ) (φ : CKN.Vec m × ℝ → ℝ) (z : CKN.Vec m × ℝ) (v : CKN.Vec m) : ℝ

The spatial gradient of a test function paired with a vector.

Equations

• CIV.gradPair m φ z v = (fderiv ℝ (fun (x : CKN.Vec m) => φ (x, z.2)) z.1) v