A continuous multilinear map with continuous-path values gives a genuine continuous path of tensors. Finite spatial coordinates establish continuity; the actual operator norm is preserved without a coordinate count in the bound.

noncomputable def EulerFinitePathTensor.coordinates {E : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (n : ℕ) : (E [×n]→L[ℝ] V) →L[ℝ] (Fin n → Fin (Module.finrank ℝ E)) → V

Coordinates, given by ContinuousLinearMap.pi (fun w => (ContinuousLinearMap.id ℝ (E [×n]→L[ℝ] V)).flipMultilinear (fun i => Module.finBasis ℝ E (w i))).

Equations

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

noncomputable def EulerFinitePathTensor.reassembly {E : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (n : ℕ) : ((Fin n → Fin (Module.finrank ℝ E)) → V) →L[ℝ] E [×n]→L[ℝ] V

Reassembly, given by ((coordinates (E := E) (V := V) n).toLinearMap.leftInverse).toContinuousLinearMap.

Equations

• EulerFinitePathTensor.reassembly n = LinearMap.toContinuousLinearMap (↑(EulerFinitePathTensor.coordinates n)).leftInverse

noncomputable def EulerFinitePathTensor.tensorPath {K : Type u_1} {E : Type u_2} {V : Type u_3} [TopologicalSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (n : ℕ) (A : E [×n]→L[ℝ] C(K, V)) : C(K, E [×n]→L[ℝ] V)

Tensor path, bundling toFun, continuous_toFun.

Equations

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

theorem EulerFinitePathTensor.tensorPath_eq {K : Type u_1} {E : Type u_2} {V : Type u_3} [TopologicalSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (n : ℕ) (A : E [×n]→L[ℝ] C(K, V)) (t : K) : (tensorPath n A) t = (ContinuousMap.evalCLM ℝ t).compContinuousMultilinearMap A

@[simp]

theorem EulerFinitePathTensor.tensorPath_apply {K : Type u_1} {E : Type u_2} {V : Type u_3} [TopologicalSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (n : ℕ) (A : E [×n]→L[ℝ] C(K, V)) (t : K) (v : Fin n → E) : ((tensorPath n A) t) v = (A v) t

theorem EulerFinitePathTensor.tensorPath_norm_le {K : Type u_1} {E : Type u_2} {V : Type u_3} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (n : ℕ) (A : E [×n]→L[ℝ] C(K, V)) : ‖tensorPath n A‖ ≤ ‖A‖

noncomputable def EulerFinitePathTensor.tensorPathLinear {K : Type u_1} {E : Type u_2} {V : Type u_3} [TopologicalSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (n : ℕ) : (E [×n]→L[ℝ] C(K, V)) →ₗ[ℝ] C(K, E [×n]→L[ℝ] V)

Tensor path linear, bundling toFun, map_add, map_smul.

Equations

• EulerFinitePathTensor.tensorPathLinear n = { toFun := EulerFinitePathTensor.tensorPath n, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def EulerFinitePathTensor.tensorPathMap {K : Type u_1} {E : Type u_2} {V : Type u_3} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (n : ℕ) : (E [×n]→L[ℝ] C(K, V)) →L[ℝ] C(K, E [×n]→L[ℝ] V)

Tensor path map, bundling toLinearMap, cont, 1.

Equations

• EulerFinitePathTensor.tensorPathMap n = { toLinearMap := EulerFinitePathTensor.tensorPathLinear n, cont := ⋯ }

@[simp]

theorem EulerFinitePathTensor.tensorPathMap_apply {K : Type u_1} {E : Type u_2} {V : Type u_3} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (n : ℕ) (A : E [×n]→L[ℝ] C(K, V)) (t : K) (v : Fin n → E) : (((tensorPathMap n) A) t) v = (A v) t

theorem EulerFinitePathTensor.tensorPath_iteratedFDeriv {K : Type u_1} {E : Type u_2} {V : Type u_3} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (f : E → C(K, V)) (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (x : E) (t : K) : ((tensorPathMap n) (iteratedFDeriv ℝ n f x)) t = iteratedFDeriv ℝ n (fun (y : E) => (f y) t) x