Fixed bounded linear maps preserve the actual spatial and time jets of smooth bounded coefficient paths.

@[instance_reducible]

noncomputable def SmoothTimeField.instSmoothTimeFieldLinear1 {E V : Type u} [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.instSmoothTimeFieldLinear1 n = inferInstance

@[instance_reducible]

noncomputable def SmoothTimeField.instSmoothTimeFieldLinear2 {E V : Type u} [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.instSmoothTimeFieldLinear2 n = inferInstance

@[instance_reducible]

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

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

Equations

• SmoothTimeField.instSmoothTimeFieldLinear3 n = inferInstance

@[instance_reducible]

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

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

Equations

• SmoothTimeField.instSmoothTimeFieldLinear4 n = inferInstance

@[instance_reducible]

noncomputable def SmoothTimeField.instSmoothTimeFieldLinear5 {E V : Type u} [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.instSmoothTimeFieldLinear5 n = inferInstance

@[instance_reducible]

noncomputable def SmoothTimeField.instSmoothTimeFieldLinear6 {E V : Type u} [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.instSmoothTimeFieldLinear6 n = inferInstance

@[instance_reducible]

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

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

Equations

• SmoothTimeField.instSmoothTimeFieldLinear7 n = inferInstance

@[instance_reducible]

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

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

Equations

• SmoothTimeField.instSmoothTimeFieldLinear8 n = inferInstance

noncomputable def SmoothTimeField.map {K E V W : Type u} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (L : V →L[ℝ] W) (A : SmoothTimeField K E V) : SmoothTimeField K E W

Map, bundling field, smooth, jet, jet_eq.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SmoothTimeField.map_apply {K E V W : Type u} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (L : V →L[ℝ] W) (A : SmoothTimeField K E V) (t : K) (x : E) : ((map L A).field t) x = L ((A.field t) x)

@[simp]

theorem SmoothTimeField.map_jet_apply {K E V W : Type u} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (L : V →L[ℝ] W) (A : SmoothTimeField K E V) (n : ℕ) (t : K) (x : E) : (((map L A).jet n) t) x = L.compContinuousMultilinearMap (((A.jet n) t) x)

theorem SmoothTimeField.map_jet_norm_le {K E V W : Type u} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (L : V →L[ℝ] W) (A : SmoothTimeField K E V) (n : ℕ) : ‖(map L A).jet n‖ ≤ ‖L‖ * ‖A.jet n‖

theorem SmoothTimeField.TimeDerivative.map {E V W : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {T : ℝ} {hT : 0 ≤ T} (L : V →L[ℝ] W) {A A₁ : SmoothTimeField (↑(Set.Icc 0 T)) E V} (h : TimeDerivative T hT A A₁) : TimeDerivative T hT (SmoothTimeField.map L A) (SmoothTimeField.map L A₁)