Polynomial coordinates of ordered products of matrix exponentials

For a list of matrices A a, List.expProdPoly gives the polynomial coordinates of the ordered product of their truncated exponentials applied to a vector parametrized by a family c of vectors. Evaluation recovers the matrix-vector product, and List.jacobiMatrixAt_expProdPoly_mulVec computes its differential when the exponential parameters vanish. The computation uses evaluation at dual numbers and requires each truncation degree to be at least two, so its constant and linear terms are retained.

noncomputable def List.expProdVec {K : Type u_1} {ι : Type u_2} {α : Type u_3} {κ : Type u_4} [Field K] [Fintype ι] [DecidableEq ι] [Fintype κ] {S : Type u_5} [CommRing S] [Algebra K S] (l : List α) (A : α → Matrix ι ι K) (d : α → ℕ) (c : κ → ι → K) (t : α → S) (s : κ → S) : ι → S

The vector (∏_{a ∈ l} exp(t_a A_a)) (∑_j s_j c_j), with the exponentials truncated below the degrees d a, for coefficients t and s in a commutative K-algebra S.

theorem List.expProdVec_def {K : Type u_1} {ι : Type u_2} {α : Type u_3} {κ : Type u_4} [Field K] [Fintype ι] [DecidableEq ι] [Fintype κ] {S : Type u_5} [CommRing S] [Algebra K S] (l : List α) (A : α → Matrix ι ι K) (d : α → ℕ) (c : κ → ι → K) (t : α → S) (s : κ → S) : l.expProdVec A d c t s = (map (fun (a : α) => (A a).expSeries (d a) (t a)) l).prod.mulVec (∑ j : κ, s j • fun (i : ι) => (algebraMap K S) (c j i))

The matrix-vector formula for the product of truncated exponentials.

@[simp]

theorem AlgHom.map_expProdVec {K : Type u_1} {ι : Type u_2} {α : Type u_3} {κ : Type u_4} [Field K] [Fintype ι] [DecidableEq ι] [Fintype κ] {S : Type u_5} {S' : Type u_6} [CommRing S] [Algebra K S] [CommRing S'] [Algebra K S'] (f : S →ₐ[K] S') (l : List α) (A : α → Matrix ι ι K) (d : α → ℕ) (c : κ → ι → K) (t : α → S) (s : κ → S) (i : ι) : f (l.expProdVec A d c t s i) = l.expProdVec A d c (⇑f ∘ t) (⇑f ∘ s) i

An algebra map commutes with an ordered product of truncated exponentials acting on a parametrized vector.

noncomputable def List.expProdPoly {K : Type u_1} {ι : Type u_2} {α : Type u_3} {κ : Type u_4} [Field K] [Fintype ι] [DecidableEq ι] [Fintype κ] (l : List α) (A : α → Matrix ι ι K) (d : α → ℕ) (c : κ → ι → K) (i : ι) : MvPolynomial (α ⊕ κ) K

The polynomial coordinates of (t, s) ↦ (∏_{a ∈ l} exp(t_a A_a)) (∑_j s_j c_j).

theorem List.expProdPoly_def {K : Type u_1} {ι : Type u_2} {α : Type u_3} {κ : Type u_4} [Field K] [Fintype ι] [DecidableEq ι] [Fintype κ] (l : List α) (A : α → Matrix ι ι K) (d : α → ℕ) (c : κ → ι → K) (i : ι) : l.expProdPoly A d c i = l.expProdVec A d c (fun (a : α) => MvPolynomial.X (Sum.inl a)) (fun (j : κ) => MvPolynomial.X (Sum.inr j)) i

The polynomial coordinates are obtained by substituting the two families of variables into List.expProdVec.

@[simp]

theorem List.eval_expProdPoly {K : Type u_1} {ι : Type u_2} {α : Type u_3} {κ : Type u_4} [Field K] [Fintype ι] [DecidableEq ι] [Fintype κ] (l : List α) (A : α → Matrix ι ι K) (d : α → ℕ) (c : κ → ι → K) (x : α ⊕ κ → K) (i : ι) : (MvPolynomial.eval x) (l.expProdPoly A d c i) = (map (fun (a : α) => (A a).expSeries (d a) (x (Sum.inl a))) l).prod.mulVec (∑ j : κ, x (Sum.inr j) • c j) i

Evaluating the polynomial coordinates recovers the ordered product of truncated exponentials applied to the vector with the given coordinates.

theorem List.jacobiMatrixAt_expProdPoly_mulVec {K : Type u_1} {ι : Type u_2} {α : Type u_3} {κ : Type u_4} [Field K] [Fintype ι] [DecidableEq ι] [Fintype κ] [Fintype α] (l : List α) (A : α → Matrix ι ι K) {d : α → ℕ} (hd : ∀ (a : α), 2 ≤ d a) (c : κ → ι → K) (s : κ → K) (w : α ⊕ κ → K) : (TauCeti.jacobiMatrixAt (l.expProdPoly A d c) (Sum.elim 0 s)).mulVec w = (map (fun (a : α) => w (Sum.inl a) • A a) l).sum.mulVec (∑ j : κ, s j • c j) + ∑ j : κ, w (Sum.inr j) • c j

The differential of the parametrization at t = 0. If every d a is at least 2, the Jacobian matrix at a point with vanishing t-coordinates sends a tangent vector w to (∑_{a ∈ l} w_a A_a) (∑_j s_j c_j) + ∑_j w_j c_j.