Smooth substitution of a continuous path into a smooth coefficient field

The derivative is the actual pointwise derivative multiplier. A uniform second-derivative remainder proves Fréchet differentiability in the path sup norm, and iteration gives smoothness at every order.

@[instance_reducible]

noncomputable def SmoothTimeField.instSmoothTimeSuperposition1 {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {V : Type u} [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.instSmoothTimeSuperposition1 n = inferInstance

@[instance_reducible]

noncomputable def SmoothTimeField.instSmoothTimeSuperposition2 {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {V : Type u} [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.instSmoothTimeSuperposition2 n = inferInstance

@[instance_reducible]

noncomputable def SmoothTimeField.instSmoothTimeSuperposition3 {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {V : Type u} [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.instSmoothTimeSuperposition3 n = inferInstance

@[instance_reducible]

noncomputable def SmoothTimeField.instSmoothTimeSuperposition4 {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {V : Type u} [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.instSmoothTimeSuperposition4 n = inferInstance

@[instance_reducible]

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

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

Equations

• SmoothTimeField.instSmoothTimeSuperposition5 n = inferInstance

@[instance_reducible]

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

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

Equations

• SmoothTimeField.instSmoothTimeSuperposition6 n = inferInstance

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

Superposition, bundling toFun, continuous_toFun.

Equations

• A.superposition u = { toFun := fun (t : K) => (A.field t) (u t), continuous_toFun := ⋯ }

@[simp]

theorem SmoothTimeField.superposition_apply {K E : Type u} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothTimeField K E V) (u : C(K, E)) (t : K) : (A.superposition u) t = (A.field t) (u t)

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

Superposition derivative, given by EulerContinuousTimeIntegral.multiplier (A.derivative.superposition u).

Equations

• A.superpositionDerivative u = EulerContinuousTimeIntegral.multiplier (A.derivative.superposition u)

theorem SmoothTimeField.superpositionDerivative_apply {K E : Type u} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothTimeField K E V) (u h : C(K, E)) (t : K) : ((A.superpositionDerivative u) h) t = (fderiv ℝ (⇑(A.field t)) (u t)) (h t)

theorem SmoothTimeField.superposition_taylor_bound {K E : Type u} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothTimeField K E V) (u v : C(K, E)) : ‖A.superposition v - A.superposition u - (A.superpositionDerivative u) (v - u)‖ ≤ ‖A.jet 2‖ * ‖v - u‖ ^ 2

theorem SmoothTimeField.superposition_hasFDerivAt {K E : Type u} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothTimeField K E V) (u : C(K, E)) : HasFDerivAt A.superposition (A.superpositionDerivative u) u

theorem SmoothTimeField.superposition_fderiv {K E : Type u} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothTimeField K E V) : fderiv ℝ A.superposition = A.superpositionDerivative

theorem SmoothTimeField.superposition_contDiff {K E : Type u} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothTimeField K E V) : ContDiff ℝ (↑⊤) A.superposition