Smooth bounded fields on a general real normed domain, with actual spatial jets continuous in the uniform time-path norm. This extends the ordinary-space coefficient interface to the lifted four-dimensional flow.

structure SmoothTimeField (K E V : Type u) [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] : Type u

Smooth time field data, collecting field, smooth, jet, jet_eq.

• field : C(K, BoundedContinuousFunction E V)

  Underlying field of SmoothTimeField, of type C(K, E →ᵇ V).

• smooth (t : K) : ContDiff ℝ ↑⊤ ⇑(self.field t)
• jet (n : ℕ) : C(K, BoundedContinuousFunction E (E [×n]→L[ℝ] V))

  Jet of SmoothTimeField, of type (n : ℕ) → C(K, E →ᵇ (E [×n]→L[ℝ] V)).

• jet_eq (n : ℕ) (t : K) (x : E) : ((self.jet n) t) x = iteratedFDeriv ℝ n (⇑(self.field t)) x

@[instance_reducible]

noncomputable def SmoothTimeField.instSmoothTimeField1 {E V : Type u} [NormedAddCommGroup E] [NormedAddCommGroup V] : NormedAddCommGroup (BoundedContinuousFunction E V)

Cache the standard NormedAddCommGroup (E →ᵇ V) instance to shorten typeclass synthesis.

Equations

• SmoothTimeField.instSmoothTimeField1 = inferInstance

@[instance_reducible]

noncomputable def SmoothTimeField.instSmoothTimeField2 {E V : Type u} [NormedAddCommGroup E] [NormedAddCommGroup V] [NormedSpace ℝ V] : NormedSpace ℝ (BoundedContinuousFunction E V)

Cache the standard NormedSpace ℝ (E →ᵇ V) instance to shorten typeclass synthesis.

Equations

• SmoothTimeField.instSmoothTimeField2 = inferInstance

@[instance_reducible]

noncomputable def SmoothTimeField.instSmoothTimeField3 {E W : Type u} [NormedAddCommGroup E] [NormedAddCommGroup W] : NormedAddCommGroup (BoundedContinuousFunction E W)

Cache the standard NormedAddCommGroup (E →ᵇ W) instance to shorten typeclass synthesis.

Equations

• SmoothTimeField.instSmoothTimeField3 = inferInstance

@[instance_reducible]

noncomputable def SmoothTimeField.instSmoothTimeField4 {E W : Type u} [NormedAddCommGroup E] [NormedAddCommGroup W] [NormedSpace ℝ W] : NormedSpace ℝ (BoundedContinuousFunction E W)

Cache the standard NormedSpace ℝ (E →ᵇ W) instance to shorten typeclass synthesis.

Equations

• SmoothTimeField.instSmoothTimeField4 = inferInstance

@[instance_reducible]

noncomputable def SmoothTimeField.instSmoothTimeField5 {E V : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] : NormedAddCommGroup (BoundedContinuousFunction E (E →L[ℝ] V))

Cache the standard NormedAddCommGroup (E →ᵇ (E →L[ℝ] V)) instance to shorten typeclass synthesis.

Equations

• SmoothTimeField.instSmoothTimeField5 = inferInstance

@[instance_reducible]

noncomputable def SmoothTimeField.instSmoothTimeField6 {E V : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] : NormedSpace ℝ (BoundedContinuousFunction E (E →L[ℝ] V))

Cache the standard NormedSpace ℝ (E →ᵇ (E →L[ℝ] V)) instance to shorten typeclass synthesis.

Equations

• SmoothTimeField.instSmoothTimeField6 = inferInstance

@[instance_reducible]

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

@[instance_reducible]

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

noncomputable def SmoothTimeField.mapPath {K E V W : Type u} [TopologicalSpace K] [NormedAddCommGroup E] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (L : V →L[ℝ] W) : C(K, BoundedContinuousFunction E V) →L[ℝ] C(K, BoundedContinuousFunction E W)

Map path, given by (L.compLeftContinuousBounded E).compLeftContinuous ℝ K.

Equations

• SmoothTimeField.mapPath L = ContinuousLinearMap.compLeftContinuous ℝ K (ContinuousLinearMap.compLeftContinuousBounded E L)

noncomputable def SmoothTimeField.derivativeField {K E V : Type u} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothTimeField K E V) : C(K, BoundedContinuousFunction E (E →L[ℝ] V))

Derivative field, given by mapPath (continuousMultilinearCurryFin1 ℝ E V).toContinuousLinearEquiv.toContinuousLinearMap (A.jet 1).

Equations

• A.derivativeField = (SmoothTimeField.mapPath ↑↑(continuousMultilinearCurryFin1 ℝ E V)) (A.jet 1)

theorem SmoothTimeField.derivativeField_eq {K E V : Type u} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothTimeField K E V) (t : K) (x : E) : (A.derivativeField t) x = fderiv ℝ (⇑(A.field t)) x

noncomputable def SmoothTimeField.derivativeJet {K E V : Type u} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothTimeField K E V) (n : ℕ) : C(K, BoundedContinuousFunction E (E [×n]→L[ℝ] E →L[ℝ] V))

Derivative jet, constructed using mapPath.

Equations

• A.derivativeJet n = (SmoothTimeField.mapPath ↑↑(continuousMultilinearCurryRightEquiv' ℝ n E V)) (A.jet (n + 1))

theorem SmoothTimeField.derivativeJet_eq {K E V : Type u} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothTimeField K E V) (n : ℕ) (t : K) (x : E) : ((A.derivativeJet n) t) x = iteratedFDeriv ℝ n (fderiv ℝ ⇑(A.field t)) x

noncomputable def SmoothTimeField.derivative {K E V : Type u} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothTimeField K E V) : SmoothTimeField K E (E →L[ℝ] V)

Derivative, bundling field, smooth, have, exact and the required compatibility proofs.

Equations

• A.derivative = { field := A.derivativeField, smooth := ⋯, jet := A.derivativeJet, jet_eq := ⋯ }

def EulerMeanCoefficients.SmoothCoefficientPath.toSmoothTimeField {K V : Type} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothCoefficientPath K V) : SmoothTimeField K EulerSmoothLimit.Space V

To smooth time field, given by ⟨A.field, A.smooth, A.jet, A.jet_eq⟩.

Equations

• A.toSmoothTimeField = { field := A.field, smooth := ⋯, jet := A.jet, jet_eq := ⋯ }

@[simp]

theorem EulerMeanCoefficients.SmoothCoefficientPath.toSmoothTimeField_field {K V : Type} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothCoefficientPath K V) : A.toSmoothTimeField.field = A.field