The actual tensor-path map commutes with the initial value and the Bochner time integral. These identities permit differentiation of a path-space integral equation at every spatial order.

theorem EulerFinitePathTensor.tensorPath_const {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {K : Type u_3} [TopologicalSpace K] [CompactSpace K] (n : ℕ) (A : E [×n]→L[ℝ] V) : (tensorPathMap n) ((ContinuousLinearMap.const ℝ K).compContinuousMultilinearMap A) = (ContinuousLinearMap.const ℝ K) A

theorem EulerFinitePathTensor.tensorPath_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) (n : ℕ) (A : E [×n]→L[ℝ] C(↑(Set.Icc 0 T), V)) : (tensorPathMap n) ((EulerContinuousTimeIntegral.integral T hT).compContinuousMultilinearMap A) = (EulerContinuousTimeIntegral.integral T hT) ((tensorPathMap n) A)