Arbitrary smoothness of primitive fields acting on continuous curves.
def
AVenhance.Infra.Section4.amnrCurveJointCompose
{K E F : Type u}
[TopologicalSpace K]
[NormedAddCommGroup E]
[NormedAddCommGroup F]
(f : ℝ × E → F)
(hf : Continuous f)
(η : C(K, ℝ))
:
Evaluate a joint primitive field along the prescribed time curve and a state trajectory. This is the actual substitution in the integral equation.
Equations
- AVenhance.Infra.Section4.amnrCurveJointCompose f hf η = AVenhance.Infra.Section4.amnrCurveCompose (fun (t : K) (x : E) => f (η t, x)) ⋯
Instances For
theorem
AVenhance.Infra.Section4.amnrCurveJointCompose_hasFDerivAt
{K E F : Type u}
[TopologicalSpace K]
[CompactSpace K]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{f : ℝ × E → F}
(hf : ContDiff ℝ (↑⊤) f)
{C : ℝ}
(hC : 0 ≤ C)
(hbound : ∀ (z : ℝ × E), ‖iteratedFDeriv ℝ 2 f z‖ ≤ C)
(η : C(K, ℝ))
(u : C(K, E))
:
HasFDerivAt (amnrCurveJointCompose f ⋯ η) (amnrCurveOperator (amnrCurveJointCompose (amnrStateDerivative f) ⋯ η u)) u
The actual joint field induces its actual curve-space derivative from a primitive second derivative bound.
theorem
AVenhance.Infra.Section4.amnrCurveJointCompose_contDiff_nat
{K E F : Type u}
[TopologicalSpace K]
[CompactSpace K]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
(n : ℕ)
{f : ℝ × E → F}
(hf : ContDiff ℝ (↑⊤) f)
(hbound : ∀ (j : ℕ), ∃ (C : ℝ), 0 ≤ C ∧ ∀ (z : ℝ × E), ‖iteratedFDeriv ℝ j f z‖ ≤ C)
(η : C(K, ℝ))
:
ContDiff ℝ (↑n) (amnrCurveJointCompose f ⋯ η)
Primitive bounds at every derivative order prove every finite order of smoothness of the substitution operator. The assumptions are actual field bounds, not regularity or bounds of the flow being constructed.
theorem
AVenhance.Infra.Section4.amnrCurveJointCompose_contDiff_infty
{K E F : Type u}
[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, ℝ))
:
ContDiff ℝ (↑⊤) (amnrCurveJointCompose f ⋯ η)
All-order primitive estimates give actual smooth substitution on the continuous-trajectory Banach space.