Genuine time product and chain rules for the constructed smooth bounded coefficient paths. The closed-interval statements include both one-sided endpoints, obtained from the actual Bochner integral identity.

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

Apply field, given by bilinear (ContinuousLinearMap.id ℝ (V →L[ℝ] W)) A B.

Equations

• A.applyField B = SmoothTimeField.bilinear (ContinuousLinearMap.id ℝ (V →L[ℝ] W)) A B

@[simp]

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

theorem SmoothTimeField.TimeDerivative.congr_fields {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₁) (he : ∀ (t : ↑(Set.Icc 0 T)) (x : E), (A.field t) x = (B.field t) x) (he₁ : ∀ (t : ↑(Set.Icc 0 T)) (x : E), (A₁.field t) x = (B₁.field t) x) : TimeDerivative T hT B B₁

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

theorem SmoothTimeField.TimeDerivative.applyField {E V W : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {T : ℝ} {hT : 0 ≤ T} {A A₁ : SmoothTimeField (↑(Set.Icc 0 T)) E (V →L[ℝ] W)} {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.applyField B) ((A₁.applyField B).add (A.applyField B₁))

theorem SmoothTimeField.compDisplacement_time_interior {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {T : ℝ} {hT : 0 ≤ T} (A A₁ : SmoothTimeField (↑(Set.Icc 0 T)) E V) (D D₁ : SmoothTimeField (↑(Set.Icc 0 T)) E E) (hA : TimeDerivative T hT A A₁) (hD : TimeDerivative T hT D D₁) (t : ↑(Set.Icc 0 T)) (ht : ↑t ∈ Set.Ioo 0 T) (x : E) : HasDerivAt (fun (s : ℝ) => realField T hT (A.compDisplacement D) s x) ((A₁.field t) (x + (D.field t) x) + ((A.derivative.field t) (x + (D.field t) x)) ((D₁.field t) x)) ↑t

theorem SmoothTimeField.TimeDerivative.compDisplacement {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {T : ℝ} {hT : 0 ≤ T} [CompleteSpace V] {A A₁ : SmoothTimeField (↑(Set.Icc 0 T)) E V} {D D₁ : SmoothTimeField (↑(Set.Icc 0 T)) E E} (hA : TimeDerivative T hT A A₁) (hD : TimeDerivative T hT D D₁) : TimeDerivative T hT (A.compDisplacement D) ((A₁.compDisplacement D).add ((A.derivative.compDisplacement D).applyField D₁))