Smooth substitution on compact trajectories from local primitive smoothness.
theorem
AVenhance.Infra.Section4.amnrCurveJointCompose_contDiff_infty_local
{K E F : Type}
[TopologicalSpace K]
[CompactSpace K]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{f : ℝ × E → F}
(hf : ContDiff ℝ (↑⊤) f)
(η : C(K, ℝ))
:
ContDiff ℝ (↑⊤) (amnrCurveJointCompose f ⋯ η)
On a compact time domain, finite-dimensional state substitution is smooth for every smooth joint field. Localization proves the needed uniform Taylor bounds; no global primitive derivative hypothesis is required.
theorem
AVenhance.Infra.Section4.amnrCurveJointCompose_fderiv_eval_local
{K E F : Type}
[TopologicalSpace K]
[CompactSpace K]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{f : ℝ × E → F}
(hf : ContDiff ℝ (↑⊤) f)
(η : C(K, ℝ))
(u v : C(K, E))
(t : K)
:
Evaluation determines the actual derivative operator of substitution from local smoothness alone.