Constants and bounded bilinear operations on actual smooth bounded coefficient paths, with the spatial product rule at every order.

@[simp]

theorem SmoothTimeField.mapPath_apply {K E : Type u} [TopologicalSpace K] [NormedAddCommGroup E] {V W : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (L : V →L[ℝ] W) (A : C(K, BoundedContinuousFunction E V)) (t : K) (x : E) : (((mapPath L) A) t) x = L ((A t) x)

noncomputable def SmoothTimeField.boundConstant {K E : Type u} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (v : V) : SmoothTimeField K E V

Bound constant, bundling field, smooth, jet, jet_eq and the required compatibility proofs.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SmoothTimeField.constant_apply {K E : Type u} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (v : V) (t : K) (x : E) : ((boundConstant v).field t) x = v

@[instance_reducible]

noncomputable def SmoothTimeField.instSmoothTimeFieldBilinear1 {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {Z : Type u} [NormedAddCommGroup Z] [NormedSpace ℝ Z] (n : ℕ) : NormedAddCommGroup (E [×n]→L[ℝ] Z)

Cache the standard NormedAddCommGroup (E [×n]→L[ℝ] Z) instance to shorten typeclass synthesis.

Equations

• SmoothTimeField.instSmoothTimeFieldBilinear1 n = inferInstance

@[instance_reducible]

noncomputable def SmoothTimeField.instSmoothTimeFieldBilinear2 {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {Z : Type u} [NormedAddCommGroup Z] [NormedSpace ℝ Z] (n : ℕ) : NormedSpace ℝ (E [×n]→L[ℝ] Z)

Cache the standard NormedSpace ℝ (E [×n]→L[ℝ] Z) instance to shorten typeclass synthesis.

Equations

• SmoothTimeField.instSmoothTimeFieldBilinear2 n = inferInstance

@[instance_reducible]

noncomputable def SmoothTimeField.instSmoothTimeFieldBilinear3 {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {Z : Type u} [NormedAddCommGroup Z] [NormedSpace ℝ Z] (n : ℕ) : NormedAddCommGroup (BoundedContinuousFunction E (E [×n]→L[ℝ] Z))

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

Equations

• SmoothTimeField.instSmoothTimeFieldBilinear3 n = inferInstance

@[instance_reducible]

noncomputable def SmoothTimeField.instSmoothTimeFieldBilinear4 {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {Z : Type u} [NormedAddCommGroup Z] [NormedSpace ℝ Z] (n : ℕ) : NormedSpace ℝ (BoundedContinuousFunction E (E [×n]→L[ℝ] Z))

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

Equations

• SmoothTimeField.instSmoothTimeFieldBilinear4 n = inferInstance

@[instance_reducible]

noncomputable def SmoothTimeField.instSmoothTimeFieldBilinear5 {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {Z : Type u} [NormedAddCommGroup Z] [NormedSpace ℝ Z] : NormedAddCommGroup (E →L[ℝ] Z)

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

Equations

• SmoothTimeField.instSmoothTimeFieldBilinear5 = inferInstance

@[instance_reducible]

noncomputable def SmoothTimeField.instSmoothTimeFieldBilinear6 {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {Z : Type u} [NormedAddCommGroup Z] [NormedSpace ℝ Z] : NormedSpace ℝ (E →L[ℝ] Z)

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

Equations

• SmoothTimeField.instSmoothTimeFieldBilinear6 = inferInstance

@[instance_reducible]

noncomputable def SmoothTimeField.instSmoothTimeFieldBilinear7 {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {Z : Type u} [NormedAddCommGroup Z] [NormedSpace ℝ Z] (n : ℕ) : NormedAddCommGroup (E [×n]→L[ℝ] E →L[ℝ] Z)

Cache the standard NormedAddCommGroup (E [×n]→L[ℝ] (E →L[ℝ] Z)) instance to shorten typeclass synthesis.

Equations

• SmoothTimeField.instSmoothTimeFieldBilinear7 n = inferInstance

@[instance_reducible]

noncomputable def SmoothTimeField.instSmoothTimeFieldBilinear8 {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {Z : Type u} [NormedAddCommGroup Z] [NormedSpace ℝ Z] (n : ℕ) : NormedSpace ℝ (E [×n]→L[ℝ] E →L[ℝ] Z)

Cache the standard NormedSpace ℝ (E [×n]→L[ℝ] (E →L[ℝ] Z)) instance to shorten typeclass synthesis.

Equations

• SmoothTimeField.instSmoothTimeFieldBilinear8 n = inferInstance

@[instance_reducible]

noncomputable def SmoothTimeField.instSmoothTimeFieldBilinear9 {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {Z : Type u} [NormedAddCommGroup Z] [NormedSpace ℝ Z] (n : ℕ) : NormedAddCommGroup (BoundedContinuousFunction E (E [×n]→L[ℝ] E →L[ℝ] Z))

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

Equations

• SmoothTimeField.instSmoothTimeFieldBilinear9 n = inferInstance

@[instance_reducible]

noncomputable def SmoothTimeField.instSmoothTimeFieldBilinear10 {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {Z : Type u} [NormedAddCommGroup Z] [NormedSpace ℝ Z] (n : ℕ) : NormedSpace ℝ (BoundedContinuousFunction E (E [×n]→L[ℝ] E →L[ℝ] Z))

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

Equations

• SmoothTimeField.instSmoothTimeFieldBilinear10 n = inferInstance

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

Bilinear path as an element of C(K,E →ᵇ Z).

Equations

• SmoothTimeField.bilinearPath B A C = { toFun := fun (t : K) => ((EulerBoundedFieldCalculus.bilinearMap B) (A.field t)) (C.field t), continuous_toFun := ⋯ }

@[simp]

theorem SmoothTimeField.bilinearPath_apply {K E : Type u} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] {V W Z : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] [NormedAddCommGroup Z] [NormedSpace ℝ Z] (B : V →L[ℝ] W →L[ℝ] Z) (A : SmoothTimeField K E V) (C : SmoothTimeField K E W) (t : K) (x : E) : ((bilinearPath B A C) t) x = (B ((A.field t) x)) ((C.field t) x)

noncomputable def SmoothTimeField.uncurryRightPath {K E : Type u} [TopologicalSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] {Z : Type u} [NormedAddCommGroup Z] [NormedSpace ℝ Z] (n : ℕ) (J : C(K, BoundedContinuousFunction E (E [×n]→L[ℝ] E →L[ℝ] Z))) : C(K, BoundedContinuousFunction E (E [×n + 1]→L[ℝ] Z))

Uncurry right path, given by mapPath (continuousMultilinearCurryRightEquiv' ℝ n E Z).symm.toContinuousLinearEquiv.toContinuousLinearMap J.

Equations

• SmoothTimeField.uncurryRightPath n J = (SmoothTimeField.mapPath ↑↑(continuousMultilinearCurryRightEquiv' ℝ n E Z).symm) J

@[simp]

theorem SmoothTimeField.uncurryRightPath_apply {K E : Type u} [TopologicalSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] {Z : Type u} [NormedAddCommGroup Z] [NormedSpace ℝ Z] (n : ℕ) (J : C(K, BoundedContinuousFunction E (E [×n]→L[ℝ] E →L[ℝ] Z))) (t : K) (x : E) : ((uncurryRightPath n J) t) x = (continuousMultilinearCurryRightEquiv' ℝ n E Z).symm ((J t) x)

theorem SmoothTimeField.exists_bilinear_jet {K E : Type u} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] {V W Z : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] [NormedAddCommGroup Z] [NormedSpace ℝ Z] (B : V →L[ℝ] W →L[ℝ] Z) (A : SmoothTimeField K E V) (C : SmoothTimeField K E W) (n : ℕ) : ∃ (J : C(K, BoundedContinuousFunction E (E [×n]→L[ℝ] Z))), ∀ (t : K) (x : E), (J t) x = iteratedFDeriv ℝ n (fun (y : E) => (B ((A.field t) y)) ((C.field t) y)) x

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

Bilinear, bundling field, smooth, jet, jet_eq.

Equations

• SmoothTimeField.bilinear B A C = { field := SmoothTimeField.bilinearPath B A C, smooth := ⋯, jet := fun (n : ℕ) => ⋯.choose, jet_eq := ⋯ }

@[simp]

theorem SmoothTimeField.bilinear_apply {K E : Type u} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] {V W Z : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] [NormedAddCommGroup Z] [NormedSpace ℝ Z] (B : V →L[ℝ] W →L[ℝ] Z) (A : SmoothTimeField K E V) (C : SmoothTimeField K E W) (t : K) (x : E) : ((bilinear B A C).field t) x = (B ((A.field t) x)) ((C.field t) x)