Time Partial

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

noncomputable def CKN.timePartial (g : Foundation.Parabolic.ParabolicPoint → ℝ) (z : Foundation.Parabolic.ParabolicPoint) : ℝ

Factor-wise time derivative on the ordinary product space described in docs/DESIGN_NOTES.md.

Equations

• CKN.timePartial g z = (fderiv ℝ (fun (s : ℝ) => g (z.1, s)) z.2) 1