Composition with identity plus a bounded smooth displacement preserves the actual continuous-time bounded spatial jets. The finite Faà di Bruno formula is evaluated in the sup norm, with no extra time derivative.

Pullback of a bounded field by identity plus a bounded displacement. Uniform spatial Lipschitz control proves continuity in the genuine sup norm.

noncomputable def EulerBoundedFieldPullback.pullback {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup V] (A : BoundedContinuousFunction E V) (d : BoundedContinuousFunction E E) : BoundedContinuousFunction E V

Pullback, constructed using BoundedContinuousFunction.ofNormedAddCommGroup.

Equations

• EulerBoundedFieldPullback.pullback A d = BoundedContinuousFunction.ofNormedAddCommGroup (fun (x : E) => A (x + d x)) ⋯ ‖A‖ ⋯

@[simp]

theorem EulerBoundedFieldPullback.pullback_apply {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup V] (A : BoundedContinuousFunction E V) (d : BoundedContinuousFunction E E) (x : E) : (pullback A d) x = A (x + d x)

theorem EulerBoundedFieldPullback.pullback_norm {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup V] (A : BoundedContinuousFunction E V) (d : BoundedContinuousFunction E E) : ‖pullback A d‖ ≤ ‖A‖

theorem EulerBoundedFieldPullback.pullback_sub_norm {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup V] (A B : BoundedContinuousFunction E V) (d e : BoundedContinuousFunction E E) (L : NNReal) (hL : LipschitzWith L ⇑A) : ‖pullback A d - pullback B e‖ ≤ ‖A - B‖ + ↑L * ‖d - e‖

theorem EulerBoundedFieldPullback.continuous_pullback {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup V] {K : Type u_3} [TopologicalSpace K] (A : C(K, BoundedContinuousFunction E V)) (d : C(K, BoundedContinuousFunction E E)) (L : NNReal) (hL : ∀ (t : K), LipschitzWith L ⇑(A t)) : Continuous fun (t : K) => pullback (A t) (d t)

noncomputable def EulerBoundedFieldPullback.pathPullback {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup V] {K : Type u_3} [TopologicalSpace K] (A : C(K, BoundedContinuousFunction E V)) (d : C(K, BoundedContinuousFunction E E)) (L : NNReal) (hL : ∀ (t : K), LipschitzWith L ⇑(A t)) : C(K, BoundedContinuousFunction E V)

Path pullback, given by ⟨fun t => pullback (A t) (d t), continuous_pullback A d L hL⟩.

Equations

• EulerBoundedFieldPullback.pathPullback A d L hL = { toFun := fun (t : K) => EulerBoundedFieldPullback.pullback (A t) (d t), continuous_toFun := ⋯ }

@[simp]

theorem EulerBoundedFieldPullback.pathPullback_apply {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup V] {K : Type u_3} [TopologicalSpace K] (A : C(K, BoundedContinuousFunction E V)) (d : C(K, BoundedContinuousFunction E E)) (L : NNReal) (hL : ∀ (t : K), LipschitzWith L ⇑(A t)) (t : K) (x : E) : ((pathPullback A d L hL) t) x = (A t) (x + (d t) x)

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

noncomputable def SmoothTimeField.instBoundedFieldPullback3 {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.instBoundedFieldPullback3 n = inferInstance

@[instance_reducible]

noncomputable def SmoothTimeField.instBoundedFieldPullback4 {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.instBoundedFieldPullback4 n = inferInstance

theorem SmoothTimeField.jet_lipschitz {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) : LipschitzWith ‖A.jet (n + 1)‖₊ ⇑((A.jet n) t)

A continuous multilinear operation acts on genuine bounded fields in the uniform norm. This includes the finite Faà di Bruno operations.

@[instance_reducible]

noncomputable def EulerBoundedFieldCalculus.instBoundedFieldMultilinear1 {α : Type u_1} {ι : Type u_2} [TopologicalSpace α] {V : ι → Type u_3} [(i : ι) → NormedAddCommGroup (V i)] (i : ι) : NormedAddCommGroup (BoundedContinuousFunction α (V i))

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

Equations

• EulerBoundedFieldCalculus.instBoundedFieldMultilinear1 i = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldCalculus.instBoundedFieldMultilinear2 {α : Type u_1} {ι : Type u_2} [TopologicalSpace α] {V : ι → Type u_3} [(i : ι) → NormedAddCommGroup (V i)] [(i : ι) → NormedSpace ℝ (V i)] (i : ι) : NormedSpace ℝ (BoundedContinuousFunction α (V i))

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

Equations

• EulerBoundedFieldCalculus.instBoundedFieldMultilinear2 i = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldCalculus.instBoundedFieldMultilinear3 {α : Type u_1} [TopologicalSpace α] {W : Type u_4} [NormedAddCommGroup W] : NormedAddCommGroup (BoundedContinuousFunction α W)

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

Equations

• EulerBoundedFieldCalculus.instBoundedFieldMultilinear3 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldCalculus.instBoundedFieldMultilinear4 {α : Type u_1} [TopologicalSpace α] {W : Type u_4} [NormedAddCommGroup W] [NormedSpace ℝ W] : NormedSpace ℝ (BoundedContinuousFunction α W)

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

Equations

• EulerBoundedFieldCalculus.instBoundedFieldMultilinear4 = inferInstance

noncomputable def EulerBoundedFieldCalculus.multilinearValue {α : Type u_1} {ι : Type u_2} [TopologicalSpace α] [Fintype ι] {V : ι → Type u_3} [(i : ι) → NormedAddCommGroup (V i)] [(i : ι) → NormedSpace ℝ (V i)] {W : Type u_4} [NormedAddCommGroup W] [NormedSpace ℝ W] (L : ContinuousMultilinearMap ℝ V W) (f : (i : ι) → BoundedContinuousFunction α (V i)) : BoundedContinuousFunction α W

Multilinear value, constructed using BoundedContinuousFunction.ofNormedAddCommGroup.

Equations

• EulerBoundedFieldCalculus.multilinearValue L f = BoundedContinuousFunction.ofNormedAddCommGroup (fun (x : α) => L fun (i : ι) => (f i) x) ⋯ (‖L‖ * ∏ i : ι, ‖f i‖) ⋯

@[simp]

theorem EulerBoundedFieldCalculus.multilinearValue_apply {α : Type u_1} {ι : Type u_2} [TopologicalSpace α] [Fintype ι] {V : ι → Type u_3} [(i : ι) → NormedAddCommGroup (V i)] [(i : ι) → NormedSpace ℝ (V i)] {W : Type u_4} [NormedAddCommGroup W] [NormedSpace ℝ W] (L : ContinuousMultilinearMap ℝ V W) (f : (i : ι) → BoundedContinuousFunction α (V i)) (x : α) : (multilinearValue L f) x = L fun (i : ι) => (f i) x

theorem EulerBoundedFieldCalculus.multilinearValue_norm {α : Type u_1} {ι : Type u_2} [TopologicalSpace α] [Fintype ι] {V : ι → Type u_3} [(i : ι) → NormedAddCommGroup (V i)] [(i : ι) → NormedSpace ℝ (V i)] {W : Type u_4} [NormedAddCommGroup W] [NormedSpace ℝ W] (L : ContinuousMultilinearMap ℝ V W) (f : (i : ι) → BoundedContinuousFunction α (V i)) : ‖multilinearValue L f‖ ≤ ‖L‖ * ∏ i : ι, ‖f i‖

noncomputable def EulerBoundedFieldCalculus.multilinearAlgebra {α : Type u_1} {ι : Type u_2} [TopologicalSpace α] [Fintype ι] {V : ι → Type u_3} [(i : ι) → NormedAddCommGroup (V i)] [(i : ι) → NormedSpace ℝ (V i)] {W : Type u_4} [NormedAddCommGroup W] [NormedSpace ℝ W] (L : ContinuousMultilinearMap ℝ V W) : MultilinearMap ℝ (fun (i : ι) => BoundedContinuousFunction α (V i)) (BoundedContinuousFunction α W)

Multilinear algebra as an element of MultilinearMap ℝ (fun i => α →ᵇ V i) (α →ᵇ W).

Equations

• EulerBoundedFieldCalculus.multilinearAlgebra L = MultilinearMap.mk' (EulerBoundedFieldCalculus.multilinearValue L) ⋯ ⋯

noncomputable def EulerBoundedFieldCalculus.multilinearMap {α : Type u_1} {ι : Type u_2} [TopologicalSpace α] [Fintype ι] {V : ι → Type u_3} [(i : ι) → NormedAddCommGroup (V i)] [(i : ι) → NormedSpace ℝ (V i)] {W : Type u_4} [NormedAddCommGroup W] [NormedSpace ℝ W] (L : ContinuousMultilinearMap ℝ V W) : ContinuousMultilinearMap ℝ (fun (i : ι) => BoundedContinuousFunction α (V i)) (BoundedContinuousFunction α W)

Multilinear map, given by (multilinearAlgebra L).mkContinuous ‖L‖ (multilinearValue_norm L).

Equations

• EulerBoundedFieldCalculus.multilinearMap L = (EulerBoundedFieldCalculus.multilinearAlgebra L).mkContinuous ‖L‖ ⋯

@[simp]

theorem EulerBoundedFieldCalculus.multilinearMap_apply {α : Type u_1} {ι : Type u_2} [TopologicalSpace α] [Fintype ι] {V : ι → Type u_3} [(i : ι) → NormedAddCommGroup (V i)] [(i : ι) → NormedSpace ℝ (V i)] {W : Type u_4} [NormedAddCommGroup W] [NormedSpace ℝ W] (L : ContinuousMultilinearMap ℝ V W) (f : (i : ι) → BoundedContinuousFunction α (V i)) (x : α) : ((multilinearMap L) f) x = L fun (i : ι) => (f i) x

theorem EulerBoundedFieldCalculus.multilinearMap_norm {α : Type u_1} {ι : Type u_2} [TopologicalSpace α] [Fintype ι] {V : ι → Type u_3} [(i : ι) → NormedAddCommGroup (V i)] [(i : ι) → NormedSpace ℝ (V i)] {W : Type u_4} [NormedAddCommGroup W] [NormedSpace ℝ W] (L : ContinuousMultilinearMap ℝ V W) : ‖multilinearMap L‖ ≤ ‖L‖

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

noncomputable def SmoothTimeField.instSmoothTimeFieldComposition3 {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.instSmoothTimeFieldComposition3 n = inferInstance

@[instance_reducible]

noncomputable def SmoothTimeField.instSmoothTimeFieldComposition4 {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.instSmoothTimeFieldComposition4 n = inferInstance

theorem SmoothTimeField.field_lipschitz {K E V : Type u} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothTimeField K E V) (t : K) : LipschitzWith ‖A.jet 1‖₊ ⇑(A.field t)

theorem SmoothTimeField.positive_identity_jet {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) (hn : 0 < n) (x : E) : iteratedFDeriv ℝ n id 0 = iteratedFDeriv ℝ n id x

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

Displaced jet, given by ContinuousMap.const K (BoundedContinuousFunction.const E (iteratedFDeriv ℝ n (id : E → E) 0)) + D.jet n.

Equations

• D.displacedJet n = ContinuousMap.const K (BoundedContinuousFunction.const E (iteratedFDeriv ℝ n id 0)) + D.jet n

theorem SmoothTimeField.displacedJet_apply {K E : Type u} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] (D : SmoothTimeField K E E) (n : ℕ) (hn : 0 < n) (t : K) (x : E) : ((D.displacedJet n) t) x = iteratedFDeriv ℝ n (fun (y : E) => y + (D.field t) y) x

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

Pulled jet, given by pathPullback (A.jet n) D.field ‖A.jet (n+1)‖₊ (A.jet_lipschitz n).

Equations

• A.pulledJet D n = EulerBoundedFieldPullback.pathPullback (A.jet n) D.field ‖A.jet (n + 1)‖₊ ⋯

@[simp]

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

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

Partition jet as an element of C(K,E →ᵇ (E [×n]→L[ℝ] V)).

Equations

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

theorem SmoothTimeField.partitionJet_apply {K E V : Type u} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothTimeField K E V) (D : SmoothTimeField K E E) {n : ℕ} (c : OrderedFinpartition n) (t : K) (x : E) : ((A.partitionJet D c) t) x = c.compAlongOrderedFinpartition (iteratedFDeriv ℝ c.length (⇑(A.field t)) (x + (D.field t) x)) fun (i : Fin c.length) => iteratedFDeriv ℝ (c.partSize i) (fun (y : E) => y + (D.field t) y) x

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

Comp displacement, 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.compDisplacement_apply {K E V : Type u} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothTimeField K E V) (D : SmoothTimeField K E E) (t : K) (x : E) : ((A.compDisplacement D).field t) x = (A.field t) (x + (D.field t) x)