Restriction of a genuine smooth time field preserves the spatial jets and the actual one-sided time derivative on a shorter interval.

@[instance_reducible]

noncomputable def SmoothTimeField.instSmoothTimeFieldRestriction1 {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (n : ℕ) : NormedAddCommGroup (E [×n]→L[ℝ] V)

Cache the standard NormedAddCommGroup (E [×n]→L[ℝ] V) instance to shorten typeclass synthesis.

Equations

• SmoothTimeField.instSmoothTimeFieldRestriction1 n = inferInstance

@[instance_reducible]

noncomputable def SmoothTimeField.instSmoothTimeFieldRestriction2 {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (n : ℕ) : NormedSpace ℝ (E [×n]→L[ℝ] V)

Cache the standard NormedSpace ℝ (E [×n]→L[ℝ] V) instance to shorten typeclass synthesis.

Equations

• SmoothTimeField.instSmoothTimeFieldRestriction2 n = inferInstance

@[instance_reducible]

noncomputable def SmoothTimeField.instSmoothTimeFieldRestriction3 {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (n : ℕ) : NormedAddCommGroup (BoundedContinuousFunction E (E [×n]→L[ℝ] V))

Cache the standard NormedAddCommGroup (E →ᵇ (E [×n]→L[ℝ] V)) instance to shorten typeclass synthesis.

Equations

• SmoothTimeField.instSmoothTimeFieldRestriction3 n = inferInstance

@[instance_reducible]

noncomputable def SmoothTimeField.instSmoothTimeFieldRestriction4 {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (n : ℕ) : NormedSpace ℝ (BoundedContinuousFunction E (E [×n]→L[ℝ] V))

Cache the standard NormedSpace ℝ (E →ᵇ (E [×n]→L[ℝ] V)) instance to shorten typeclass synthesis.

Equations

• SmoothTimeField.instSmoothTimeFieldRestriction4 n = inferInstance

noncomputable def SmoothTimeField.compTime {K J E V : Type} [TopologicalSpace K] [CompactSpace K] [TopologicalSpace J] [CompactSpace J] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothTimeField K E V) (f : C(J, K)) : SmoothTimeField J E V

Comp time, bundling field, smooth, jet, jet_eq.

Equations

• A.compTime f = { field := A.field.comp f, smooth := ⋯, jet := fun (n : ℕ) => (A.jet n).comp f, jet_eq := ⋯ }

@[simp]

theorem SmoothTimeField.compTime_apply {K J E V : Type} [TopologicalSpace K] [CompactSpace K] [TopologicalSpace J] [CompactSpace J] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothTimeField K E V) (f : C(J, K)) (t : J) (x : E) : ((A.compTime f).field t) x = (A.field (f t)) x

theorem SmoothTimeField.compTime_jet_norm {K J E V : Type} [TopologicalSpace K] [CompactSpace K] [TopologicalSpace J] [CompactSpace J] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothTimeField K E V) (f : C(J, K)) (n : ℕ) : ‖(A.compTime f).jet n‖ ≤ ‖A.jet n‖

theorem SmoothTimeField.TimeDerivative.restrictInitial {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {T S : ℝ} {hT : 0 ≤ T} (hS : 0 ≤ S) (hST : S ≤ T) {A B : SmoothTimeField (↑(Set.Icc 0 T)) E V} (h : TimeDerivative T hT A B) : TimeDerivative S hS (A.compTime (EulerTimeIntervalRestriction.initialInclusion T S hST)) (B.compTime (EulerTimeIntervalRestriction.initialInclusion T S hST))