Dz

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

noncomputable def CIV.dz (φ : (ℝ × ℝ) × ℝ → ℝ) (p : (ℝ × ℝ) × ℝ) : ℝ

∂_z of a function of ((r, z), t).

Equations

• CIV.dz φ p = deriv (fun (z : ℝ) => φ ((p.1.1, z), p.2)) p.1.2