Classical derivatives from weak time derivatives

On an open interval, a continuous function with a continuous weak derivative has that derivative classically. This is the time-calculus step in the regularized momentum equation of thm:regularised (R2).

theorem CKN.Leray.regularisedR12TimeCore_hasDerivAt_of_weakDeriv (T : ℝ) (hT : 0 < T) {f g : ℝ → ℝ} (hf : ContinuousOn f (Set.Ioo 0 T)) (hg : ContinuousOn g (Set.Ioo 0 T)) (hweak : HasWeakDerivOn (Set.Ioo 0 T) f g) (t : ℝ) : t ∈ Set.Ioo 0 T → HasDerivAt f (g t) t

A continuous weak time derivative agrees with the classical derivative at every interior point of a finite positive-time interval.