Addition of actual smooth bounded fields and their genuine time jets.

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

noncomputable def SmoothTimeField.add {K E V : Type u} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (A B : SmoothTimeField K E V) : SmoothTimeField K E V

Add, bundling field, smooth, jet, jet_eq.

Equations

• A.add B = { field := A.field + B.field, smooth := ⋯, jet := fun (n : ℕ) => A.jet n + B.jet n, jet_eq := ⋯ }

@[simp]

theorem SmoothTimeField.add_apply {K E V : Type u} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (A B : SmoothTimeField K E V) (t : K) (x : E) : ((A.add B).field t) x = (A.field t) x + (B.field t) x

theorem SmoothTimeField.add_jet_norm_le {K E V : Type u} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (A B : SmoothTimeField K E V) (n : ℕ) : ‖(A.add B).jet n‖ ≤ ‖A.jet n‖ + ‖B.jet n‖

theorem SmoothTimeField.jet_eq_of_field_eq {K E V : Type u} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (A B : SmoothTimeField K E V) (h : ∀ (t : K) (x : E), (A.field t) x = (B.field t) x) (n : ℕ) : A.jet n = B.jet n

theorem SmoothTimeField.TimeDerivative.add {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {T : ℝ} {hT : 0 ≤ T} {A A₁ B B₁ : SmoothTimeField (↑(Set.Icc 0 T)) E V} (hA : TimeDerivative T hT A A₁) (hB : TimeDerivative T hT B B₁) : TimeDerivative T hT (A.add B) (A₁.add B₁)