Genuine linear restriction of smooth coefficient fields, including the exact spatial tensors and preservation of actual time derivatives.

@[instance_reducible]

noncomputable def SmoothTimeField.instSmoothTimeFieldPrecomp1 {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.instSmoothTimeFieldPrecomp1 n = inferInstance

@[instance_reducible]

noncomputable def SmoothTimeField.instSmoothTimeFieldPrecomp2 {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.instSmoothTimeFieldPrecomp2 n = inferInstance

@[instance_reducible]

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

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

Equations

• SmoothTimeField.instSmoothTimeFieldPrecomp3 n = inferInstance

@[instance_reducible]

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

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

Equations

• SmoothTimeField.instSmoothTimeFieldPrecomp4 n = inferInstance

@[instance_reducible]

noncomputable def SmoothTimeField.instSmoothTimeFieldPrecomp5 {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.instSmoothTimeFieldPrecomp5 n = inferInstance

@[instance_reducible]

noncomputable def SmoothTimeField.instSmoothTimeFieldPrecomp6 {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.instSmoothTimeFieldPrecomp6 n = inferInstance

@[instance_reducible]

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

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

Equations

• SmoothTimeField.instSmoothTimeFieldPrecomp7 n = inferInstance

@[instance_reducible]

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

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

Equations

• SmoothTimeField.instSmoothTimeFieldPrecomp8 n = inferInstance

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

Precomp linear, bundling field, smooth, jet, jet_eq and the required compatibility proofs.

Equations

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

@[simp]

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

@[simp]

theorem SmoothTimeField.precompLinear_jet_apply {K E F V : Type u} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothTimeField K E V) (L : F →L[ℝ] E) (n : ℕ) (t : K) (x : F) : (((A.precompLinear L).jet n) t) x = (((A.jet n) t) (L x)).compContinuousLinearMap fun (x : Fin n) => L

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

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