Dr

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

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

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

Equations

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