Factor-wise derivatives of height and time functions

The scalar derivatives of a height-dependent cutoff agree with its spatial derivatives in the normal coordinate.

theorem ESS.bu_spatialPartial_height (g : ℝ → ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) (hgd : DifferentiableAt ℝ g (z.1 2)) (j : Fin 3) : CKN.spatialPartial (fun (q : CKN.Foundation.Parabolic.ParabolicPoint) => g (q.1 2)) j z = deriv g (z.1 2) * if j = 2 then 1 else 0

A scalar function of height has only one spatial derivative.

theorem ESS.bu_spatialSecondPartial_height_diag (g : ℝ → ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) (hgd : Differentiable ℝ g) (hdd : DifferentiableAt ℝ (deriv g) (z.1 2)) (j : Fin 3) : CKN.spatialSecondPartial (fun (q : CKN.Foundation.Parabolic.ParabolicPoint) => g (q.1 2)) j j z = if j = 2 then deriv (deriv g) (z.1 2) else 0

The diagonal second spatial derivatives of a height function are zero except in the normal coordinate.

theorem ESS.bu_timePartial_time (g : ℝ → ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) : CKN.timePartial (fun (q : CKN.Foundation.Parabolic.ParabolicPoint) => g q.2) z = deriv g z.2

A scalar function of time has the expected time partial derivative.