An actual smooth family of time paths carries the differentiated time equation at every spatial order. This is proved by the bounded Bochner integral identity, rather than assumed commutation of derivatives.

noncomputable def EulerSmoothPathTimeJets.jetFamily {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (T : ℝ) (f : E → C(↑(Set.Icc 0 T), V)) (n : ℕ) (x : E) : C(↑(Set.Icc 0 T), E [×n]→L[ℝ] V)

Jet family, given by tensorPathMap n (iteratedFDeriv ℝ n f x).

Equations

• EulerSmoothPathTimeJets.jetFamily T f n x = (EulerFinitePathTensor.tensorPathMap n) (iteratedFDeriv ℝ n f x)

theorem EulerSmoothPathTimeJets.jetFamily_contDiff {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (T : ℝ) (f : E → C(↑(Set.Icc 0 T), V)) (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) : ContDiff ℝ (↑⊤) (jetFamily T f n)

theorem EulerSmoothPathTimeJets.jetFamily_apply {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (T : ℝ) (f : E → C(↑(Set.Icc 0 T), V)) (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (x : E) (t : ↑(Set.Icc 0 T)) : (jetFamily T f n x) t = iteratedFDeriv ℝ n (fun (y : E) => (f y) t) x

theorem EulerSmoothPathTimeJets.jetFamily_integral {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (T : ℝ) (hT : 0 ≤ T) (f q : E → C(↑(Set.Icc 0 T), V)) (hf : ContDiff ℝ (↑⊤) f) (hq : ContDiff ℝ (↑⊤) q) (hd : ∀ (x : E) (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (f x)) ((q x) t) (Set.Icc 0 T) ↑t) (n : ℕ) (x : E) : jetFamily T f n x = (ContinuousLinearMap.const ℝ ↑(Set.Icc 0 T)) ((ContinuousMap.evalCLM ℝ ⟨0, ⋯⟩).compContinuousMultilinearMap (iteratedFDeriv ℝ n f x)) + (EulerContinuousTimeIntegral.integral T hT) (jetFamily T q n x)

theorem EulerSmoothPathTimeJets.jetFamily_hasDerivWithinAt {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (T : ℝ) (hT : 0 ≤ T) (f q : E → C(↑(Set.Icc 0 T), V)) (hf : ContDiff ℝ (↑⊤) f) (hq : ContDiff ℝ (↑⊤) q) (hd : ∀ (x : E) (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (f x)) ((q x) t) (Set.Icc 0 T) ↑t) (n : ℕ) (x : E) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (jetFamily T f n x)) ((jetFamily T q n x) t) (Set.Icc 0 T) ↑t