Actual spatial derivatives and their inherited initial trace.

theorem AVenhance.Infra.Section4.amnr_energy_spatial_partial_smooth_up_to_initial {f : AmnrSpace → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (Set.Ici 0 ×ˢ Set.univ)) (i : Fin 2) : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => spaceGrad (fun (y : Homogenization.Vec 2) => f (z.1, y)) z.2 i) (Set.Ici 0 ×ˢ Set.univ)

Differentiate only in space on the closed nonnegative-time domain.

theorem AVenhance.Infra.Section4.amnrSpaceWord_smooth_up_to_initial {u : ℝ → Homogenization.Vec 2 → ℝ} (hu : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => u z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (w : List (Fin 2)) : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => amnrSpaceWord w (u z.1) z.2) (Set.Ici 0 ×ˢ Set.univ)

All ordered spatial derivatives of the actual scalar retain joint smoothness on the closed time domain, including their initial trace.