Actual time identities for all spatial jets of the constructed flow

The spatial derivative is taken in the full continuous-path Banach space. The bounded time integral commutes with it at every order. Reassembling the tensor paths therefore gives genuine within-time derivatives of all jets, without assuming differentiability of an ODE solution family.

noncomputable def EulerSmoothBanachFlow.velocityFamily {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (x : E) : C(↑(Set.Icc 0 T), E)

Velocity family, given by A.superposition (pathFamily T hT A x).

Equations

• EulerSmoothBanachFlow.velocityFamily T hT A x = A.superposition ((EulerSmoothBanachFlow.pathFamily T hT A) x)

theorem EulerSmoothBanachFlow.velocityFamily_contDiff {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) : ContDiff ℝ (↑⊤) (velocityFamily T hT A)

noncomputable def EulerSmoothBanachFlow.displacementFamily {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (x : E) : C(↑(Set.Icc 0 T), E)

Displacement family, given by pathFamily T hT A x - (ContinuousLinearMap.const ℝ (Icc (0 : ℝ) T)) x.

Equations

• EulerSmoothBanachFlow.displacementFamily T hT A x = (EulerSmoothBanachFlow.pathFamily T hT A) x - (ContinuousLinearMap.const ℝ ↑(Set.Icc 0 T)) x

theorem EulerSmoothBanachFlow.displacementFamily_contDiff {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) : ContDiff ℝ (↑⊤) (displacementFamily T hT A)

theorem EulerSmoothBanachFlow.displacementFamily_integral {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (x : E) : displacementFamily T hT A x = (EulerContinuousTimeIntegral.integral T hT) (velocityFamily T hT A x)

noncomputable def EulerSmoothBanachFlow.jetPath {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (n : ℕ) (x : E) : C(↑(Set.Icc 0 T), E [×n]→L[ℝ] E)

Jet path, given by tensorPathMap n (iteratedFDeriv ℝ n (pathFamily T hT A) x).

Equations

• EulerSmoothBanachFlow.jetPath T hT A n x = (EulerFinitePathTensor.tensorPathMap n) (iteratedFDeriv ℝ n (⇑(EulerSmoothBanachFlow.pathFamily T hT A)) x)

noncomputable def EulerSmoothBanachFlow.velocityJetPath {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (n : ℕ) (x : E) : C(↑(Set.Icc 0 T), E [×n]→L[ℝ] E)

Velocity jet path, given by tensorPathMap n (iteratedFDeriv ℝ n (velocityFamily T hT A) x).

Equations

• EulerSmoothBanachFlow.velocityJetPath T hT A n x = (EulerFinitePathTensor.tensorPathMap n) (iteratedFDeriv ℝ n (EulerSmoothBanachFlow.velocityFamily T hT A) x)

noncomputable def EulerSmoothBanachFlow.displacementJetPath {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (n : ℕ) (x : E) : C(↑(Set.Icc 0 T), E [×n]→L[ℝ] E)

Displacement jet path, given by tensorPathMap n (iteratedFDeriv ℝ n (displacementFamily T hT A) x).

Equations

• EulerSmoothBanachFlow.displacementJetPath T hT A n x = (EulerFinitePathTensor.tensorPathMap n) (iteratedFDeriv ℝ n (EulerSmoothBanachFlow.displacementFamily T hT A) x)

theorem EulerSmoothBanachFlow.jetPath_apply {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (n : ℕ) (x : E) (t : ↑(Set.Icc 0 T)) : (jetPath T hT A n x) t = iteratedFDeriv ℝ n (fun (y : E) => (flowData T hT A).forward (↑t) y) x

theorem EulerSmoothBanachFlow.velocityJetPath_apply {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (n : ℕ) (x : E) (t : ↑(Set.Icc 0 T)) : (velocityJetPath T hT A n x) t = iteratedFDeriv ℝ n (fun (y : E) => (A.field t) ((flowData T hT A).forward (↑t) y)) x

theorem EulerSmoothBanachFlow.displacementJetPath_integral {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (n : ℕ) (x : E) : displacementJetPath T hT A n x = (EulerContinuousTimeIntegral.integral T hT) (velocityJetPath T hT A n x)

theorem EulerSmoothBanachFlow.displacementJetPath_hasDerivWithinAt {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (n : ℕ) (x : E) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (displacementJetPath T hT A n x)) ((velocityJetPath T hT A n x) t) (Set.Icc 0 T) ↑t

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

The clamped extension is used only to state derivatives on the closed time interval; there it is exactly the constructed flow minus its label.

Equations

• EulerSmoothBanachFlow.displacement T hT A t x = EulerVolterraConvolution.extendPath T hT (EulerSmoothBanachFlow.displacementFamily T hT A x) t

theorem EulerSmoothBanachFlow.displacement_eq {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (t : ↑(Set.Icc 0 T)) (x : E) : displacement T hT A (↑t) x = (flowData T hT A).forward (↑t) x - x

theorem EulerSmoothBanachFlow.displacement_contDiff {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (t : ℝ) : ContDiff ℝ (↑⊤) (displacement T hT A t)

theorem EulerSmoothBanachFlow.displacement_zero {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) : displacement T hT A 0 = 0

theorem EulerSmoothBanachFlow.displacementJetPath_apply {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (n : ℕ) (x : E) (t : ℝ) : EulerVolterraConvolution.extendPath T hT (displacementJetPath T hT A n x) t = iteratedFDeriv ℝ n (displacement T hT A t) x

theorem EulerSmoothBanachFlow.velocityJetPath_displacement {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (n : ℕ) (x : E) (t : ↑(Set.Icc 0 T)) : (velocityJetPath T hT A n x) t = iteratedFDeriv ℝ n (fun (y : E) => (A.field t) (y + displacement T hT A (↑t) y)) x

theorem EulerSmoothBanachFlow.displacement_jet_hasDerivWithinAt {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (n : ℕ) (x : E) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (fun (s : ℝ) => iteratedFDeriv ℝ n (displacement T hT A s) x) (iteratedFDeriv ℝ n (fun (y : E) => (A.field t) (y + displacement T hT A (↑t) y)) x) (Set.Icc 0 T) ↑t

Every actual spatial tensor has the differentiated ODE as its genuine time derivative, including one-sided derivatives at both endpoints.

theorem EulerSmoothBanachFlow.displacement_jet_continuous {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (n : ℕ) (x : E) : Continuous fun (t : ℝ) => iteratedFDeriv ℝ n (displacement T hT A t) x

theorem EulerSmoothBanachFlow.velocity_jet_continuous {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (n : ℕ) (x : E) : Continuous fun (t : ↑(Set.Icc 0 T)) => iteratedFDeriv ℝ n (fun (y : E) => (A.field t) (y + displacement T hT A (↑t) y)) x