A literal time derivative of smooth bounded fields differentiates every actual spatial jet, both pointwise and in the uniform field norm.

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

def SmoothTimeField.sliceFamily {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (T : ℝ) (A : SmoothTimeField (↑(Set.Icc 0 T)) E V) (x : E) : C(↑(Set.Icc 0 T), V)

Slice family, given by A.superposition ((ContinuousLinearMap.const ℝ (Icc (0 : ℝ) T)) x).

Equations

• SmoothTimeField.sliceFamily T A x = A.superposition ((ContinuousLinearMap.const ℝ ↑(Set.Icc 0 T)) x)

@[simp]

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

theorem SmoothTimeField.sliceFamily_contDiff {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (T : ℝ) (A : SmoothTimeField (↑(Set.Icc 0 T)) E V) : ContDiff ℝ (↑⊤) (sliceFamily T A)

theorem SmoothTimeField.sliceFamily_jet {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (T : ℝ) (A : SmoothTimeField (↑(Set.Icc 0 T)) E V) (n : ℕ) (x : E) (t : ↑(Set.Icc 0 T)) : (EulerSmoothPathTimeJets.jetFamily T (sliceFamily T A) n x) t = ((A.jet n) t) x

theorem SmoothTimeField.TimeDerivative.jet_pointwise {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (T : ℝ) (hT : 0 ≤ T) (A A₁ : SmoothTimeField (↑(Set.Icc 0 T)) E V) (htime : TimeDerivative T hT A A₁) (n : ℕ) (x : E) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (fun (s : ℝ) => (EulerVolterraConvolution.extendPath T hT (A.jet n) s) x) (((A₁.jet n) t) x) (Set.Icc 0 T) ↑t

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

theorem SmoothTimeField.TimeDerivative.jet_uniform {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (T : ℝ) (hT : 0 ≤ T) (A A₁ : SmoothTimeField (↑(Set.Icc 0 T)) E V) (htime : TimeDerivative T hT A A₁) (n : ℕ) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (A.jet n)) ((A₁.jet n) t) (Set.Icc 0 T) ↑t