Actual higher derivatives of primitive fields acting on trajectories.
theorem
AVenhance.Infra.Section4.amnrCurveJointCompose_iteratedFDeriv_eval
{K E F : Type}
[TopologicalSpace K]
[CompactSpace K]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{f : ℝ × E → F}
(hf : ContDiff ℝ (↑⊤) f)
(hbound : ∀ (j : ℕ), ∃ (C : ℝ), 0 ≤ C ∧ ∀ (z : ℝ × E), ‖iteratedFDeriv ℝ j f z‖ ≤ C)
(η : C(K, ℝ))
(n : ℕ)
(u : C(K, E))
(v : Fin n → C(K, E))
(t : K)
:
((iteratedFDeriv ℝ n (amnrCurveJointCompose f ⋯ η) u) v) t = (iteratedFDeriv ℝ n (fun (x : E) => f (η t, x)) (u t)) fun (j : Fin n) => (v j) t
Each actual trajectory-space derivative is the pointwise state derivative of the primitive field. There is no additional norm cost from the curve-space representation.
theorem
AVenhance.Infra.Section4.amnrCurveJointCompose_iteratedFDeriv_norm_le
{K E F : Type}
[TopologicalSpace K]
[CompactSpace K]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{f : ℝ × E → F}
(hf : ContDiff ℝ (↑⊤) f)
(hbound : ∀ (j : ℕ), ∃ (C : ℝ), 0 ≤ C ∧ ∀ (z : ℝ × E), ‖iteratedFDeriv ℝ j f z‖ ≤ C)
(η : C(K, ℝ))
(n : ℕ)
(u : C(K, E))
{B : ℝ}
(hB : 0 ≤ B)
(hstate : ∀ (t : K) (x : E), ‖iteratedFDeriv ℝ n (fun (y : E) => f (η t, y)) x‖ ≤ B)
:
A uniform actual state-derivative bound gives exactly the same bound for the corresponding operator on continuous trajectories.