Time Deriv

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

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

The time derivative of a test function on Vec m × ℝ.

Equations

• CIV.timeDeriv m φ z = (fderiv ℝ (fun (τ : ℝ) => φ (z.1, τ)) z.2) 1