Dt Past

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

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

The one-sided (from the past) time derivative of a function of ((r, z), t).

Equations

• CIV.dtPast φ p = derivWithin (fun (t : ℝ) => φ (p.1, t)) (Set.Iic p.2) p.2