Actual time derivatives and the genuine spatial jets give joint C¹ regularity on the interior of the time interval.

noncomputable def SmoothTimeField.realField {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E V) (t : ℝ) (x : E) : V

Real field, given by extendPath T hT A.field t x.

Equations

• SmoothTimeField.realField T hT A t x = (EulerVolterraConvolution.extendPath T hT A.field t) x

@[simp]

theorem SmoothTimeField.realField_apply {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E V) (t : ↑(Set.Icc 0 T)) (x : E) : realField T hT A (↑t) x = (A.field t) x

theorem SmoothTimeField.realField_joint_continuous {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E V) : Continuous (Function.uncurry (realField T hT A))

def SmoothTimeField.TimeDerivative {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (T : ℝ) (hT : 0 ≤ T) (A A₁ : SmoothTimeField (↑(Set.Icc 0 T)) E V) : Prop

Time derivative, given by ∀ t : Icc (0 : ℝ) T, ∀ x : E, HasDerivWithinAt (fun s => A.realField T hT s x) (A₁.field t x) (Icc (0 : ℝ) T) t.

Equations

• SmoothTimeField.TimeDerivative T hT A A₁ = ∀ (t : ↑(Set.Icc 0 T)) (x : E), HasDerivWithinAt (fun (s : ℝ) => SmoothTimeField.realField T hT A s x) ((A₁.field t) x) (Set.Icc 0 T) ↑t

noncomputable def SmoothTimeField.jointDerivative {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (T : ℝ) (hT : 0 ≤ T) (A A₁ : SmoothTimeField (↑(Set.Icc 0 T)) E V) (t : ℝ) (x : E) : ℝ × E →L[ℝ] V

Joint derivative, given by (ContinuousLinearMap.toSpanSingleton ℝ (A₁.realField T hT t x)).coprod (A.derivative.realField T hT t x).

Equations

• SmoothTimeField.jointDerivative T hT A A₁ t x = (ContinuousLinearMap.toSpanSingleton ℝ (SmoothTimeField.realField T hT A₁ t x)).coprod (SmoothTimeField.realField T hT A.derivative t x)

theorem SmoothTimeField.jointDerivative_continuous {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (T : ℝ) (hT : 0 ≤ T) (A A₁ : SmoothTimeField (↑(Set.Icc 0 T)) E V) : Continuous (Function.uncurry (jointDerivative T hT A A₁))

theorem SmoothTimeField.realField_hasFDerivAt {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (T : ℝ) (hT : 0 ≤ T) (A A₁ : SmoothTimeField (↑(Set.Icc 0 T)) E V) (htime : TimeDerivative T hT A A₁) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) (x : E) : HasFDerivAt (Function.uncurry (realField T hT A)) (jointDerivative T hT A A₁ t x) (t, x)

theorem SmoothTimeField.realField_contDiffAt_one {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (T : ℝ) (hT : 0 ≤ T) (A A₁ : SmoothTimeField (↑(Set.Icc 0 T)) E V) (htime : TimeDerivative T hT A A₁) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) (x : E) : ContDiffAt ℝ 1 (Function.uncurry (realField T hT A)) (t, x)