Joint continuous differentiability from continuous partial derivatives

A space-time field whose spatial slices are differentiable, whose coordinate spatial partial derivatives are continuous, and whose time derivative exists and is continuous on ℝ³ × (0,∞) is continuously differentiable there as a function of the space-time point. This gives the joint C¹ clause of thm:regularised (R2).

theorem CKN.Leray.regR12_contDiffOn_one_of_partials (f g : Foundation.Parabolic.ParabolicPoint → ℝ) (hdiff : ∀ z ∈ spaceTimeSet Set.univ (Set.Ioi 0), DifferentiableAt ℝ (fun (x : Foundation.Parabolic.Vec3) => f (x, z.2)) z.1) (hD : ∀ (j : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => spatialPartial f j z) (spaceTimeSet Set.univ (Set.Ioi 0))) (ht : ∀ z ∈ spaceTimeSet Set.univ (Set.Ioi 0), HasDerivAt (fun (s : ℝ) => f (z.1, s)) (g z) z.2) (hg : ContinuousOn g (spaceTimeSet Set.univ (Set.Ioi 0))) : ContDiffOn ℝ 1 f (spaceTimeSet Set.univ (Set.Ioi 0))

thm:regularised (R2), joint C¹: continuous spatial partial derivatives and a continuous time derivative give joint continuous differentiability on ℝ³ × (0,∞).