Coefficient families for the product of two state-affine systems
DefinitionPolyAssemblyThis module supplies the coefficient bookkeeping behind the closure of state-affine systems under products.
The blocks are polynomial. Writing for a coefficient family, each block of the product system is itself the evaluation of a coefficient family, obtained by convolving degrees:
and likewise for the left cross block and for the purely affine block . These are the analogues, for the cross and affine blocks, of equation (3.20) of the source, which covers the tensor block.
The index type. Each family of blocks carries its own degree, so the coefficients of the product system are indexed by a disjoint union: one index per coefficient of , one per coefficient of , and one per pair of coefficients for the cross and tensor blocks, whose degree is the sum. Uniformizing all degrees over pairs would force writing the diagonal blocks as "only when the second index is zero", which is both less readable and harder to manipulate.
Formalization Note The three evaluation identities are proved; crossCoef and prodCoef are definitions, so nothing here asserts that they are correct in any sense — that is the content of the accompanying theorem. Coefficient families are indexed by Fin r, so both factors carry the same number of coefficients; padding by zero accommodates a shorter one. The Kronecker map is the entrywise product, and the tensor of two vectors the pointwise product over the pair index.
import Mathlib
import Definitions.Def_SASAlgebra
set_option autoImplicit false
set_option maxHeartbeats 1000000
open Matrix SASAlgebra
namespace PolyAssembly
variable {N₁ N₂ r : ℕ}
/-- Le bloc croise droit est polynomial : `Σ_{m,n} z^{m+n} (P¹ₘ ⊗ Q²ₙ) = p₁(z) ⊗ q₂(z)`. -/
theorem kronRight_eval (P₁ : Fin r → Matrix (Fin N₁) (Fin N₁) ℝ)
(Q₂ : Fin r → (Fin N₂ → ℝ)) (z : ℝ) :
∑ mn : Fin r × Fin r, (z ^ ((mn.1 : ℕ) + (mn.2 : ℕ))) • kronRight (P₁ mn.1) (Q₂ mn.2)
= kronRight (polyEval P₁ z) (vpolyEval Q₂ z) := by
ext ij a
simp only [kronRight, polyEval, vpolyEval, Matrix.sum_apply, Finset.sum_apply,
Matrix.smul_apply, Pi.smul_apply, smul_eq_mul, Fintype.sum_prod_type]
rw [Finset.sum_mul_sum]
exact Finset.sum_congr rfl (fun m _ => Finset.sum_congr rfl (fun n _ => by
rw [pow_add]; ring))
/-- Le bloc croise gauche est polynomial : `Σ_{m,n} z^{m+n} (Q¹ₘ ⊗ P²ₙ) = q₁(z) ⊗ p₂(z)`. -/
theorem kronLeft_eval (Q₁ : Fin r → (Fin N₁ → ℝ))
(P₂ : Fin r → Matrix (Fin N₂) (Fin N₂) ℝ) (z : ℝ) :
∑ mn : Fin r × Fin r, (z ^ ((mn.1 : ℕ) + (mn.2 : ℕ))) • kronLeft (Q₁ mn.1) (P₂ mn.2)
= kronLeft (vpolyEval Q₁ z) (polyEval P₂ z) := by
ext ij a
simp only [kronLeft, polyEval, vpolyEval, Matrix.sum_apply, Finset.sum_apply,
Matrix.smul_apply, Pi.smul_apply, smul_eq_mul, Fintype.sum_prod_type]
rw [Finset.sum_mul_sum]
exact Finset.sum_congr rfl (fun m _ => Finset.sum_congr rfl (fun n _ => by
rw [pow_add]; ring))
/-- Le terme affine tensoriel est polynomial : `Σ_{m,n} z^{m+n} (Q¹ₘ ⊗ Q²ₙ) = q₁(z) ⊗ q₂(z)`. -/
theorem vkron_eval (Q₁ : Fin r → (Fin N₁ → ℝ)) (Q₂ : Fin r → (Fin N₂ → ℝ)) (z : ℝ) :
∑ mn : Fin r × Fin r, (z ^ ((mn.1 : ℕ) + (mn.2 : ℕ))) • vkron (Q₁ mn.1) (Q₂ mn.2)
= vkron (vpolyEval Q₁ z) (vpolyEval Q₂ z) := by
funext ij
simp only [vkron, vpolyEval, Finset.sum_apply, Pi.smul_apply, smul_eq_mul,
Fintype.sum_prod_type]
rw [Finset.sum_mul_sum]
exact Finset.sum_congr rfl (fun m _ => Finset.sum_congr rfl (fun n _ => by
rw [pow_add]; ring))
/-! ### Assemblage
Tous les blocs s'indexent uniformement par les couples `(m,n)` de degres, avec le degre
`m + n` : les blocs diagonaux, de degre simple, se voient comme des blocs de degre
`m + n` dont seuls les termes `n = 0` (respectivement `m = 0`) sont non nuls. -/
/-- Le bloc croise, coefficient par coefficient. -/
noncomputable def crossCoef (P₁ : Fin r → Matrix (Fin N₁) (Fin N₁) ℝ)
(Q₁ : Fin r → (Fin N₁ → ℝ)) (P₂ : Fin r → Matrix (Fin N₂) (Fin N₂) ℝ)
(Q₂ : Fin r → (Fin N₂ → ℝ)) (mn : Fin r × Fin r) :
Matrix (Fin N₁ × Fin N₂) (Fin N₁ ⊕ Fin N₂) ℝ :=
Matrix.of fun ij a => Sum.elim (fun a₁ => kronRight (P₁ mn.1) (Q₂ mn.2) ij a₁)
(fun a₂ => kronLeft (Q₁ mn.1) (P₂ mn.2) ij a₂) a
/-- Le type d'indices du systeme produit : un indice par bloc, avec son degre propre. -/
abbrev ProdIdx (r : ℕ) := (Fin r ⊕ Fin r) ⊕ (Fin r × Fin r)
/-- Le degre de chaque coefficient : simple pour les blocs diagonaux, somme pour les
blocs croises et tensoriel. -/
def prodDeg {r : ℕ} : ProdIdx r → ℕ
| Sum.inl (Sum.inl m) => (m : ℕ)
| Sum.inl (Sum.inr n) => (n : ℕ)
| Sum.inr mn => (mn.1 : ℕ) + (mn.2 : ℕ)
/-- **Les coefficients du systeme produit.** Une seule famille, dont l'evaluation en `z`
redonne la matrice du systeme produit. -/
noncomputable def prodCoef (P₁ : Fin r → Matrix (Fin N₁) (Fin N₁) ℝ)
(Q₁ : Fin r → (Fin N₁ → ℝ)) (P₂ : Fin r → Matrix (Fin N₂) (Fin N₂) ℝ)
(Q₂ : Fin r → (Fin N₂ → ℝ)) : ProdIdx r →
Matrix ((Fin N₁ ⊕ Fin N₂) ⊕ (Fin N₁ × Fin N₂))
((Fin N₁ ⊕ Fin N₂) ⊕ (Fin N₁ × Fin N₂)) ℝ
| Sum.inl (Sum.inl m) =>
Matrix.fromBlocks (Matrix.fromBlocks (P₁ m) 0 0 0) 0 0 0
| Sum.inl (Sum.inr n) =>
Matrix.fromBlocks (Matrix.fromBlocks 0 0 0 (P₂ n)) 0 0 0
| Sum.inr mn =>
Matrix.fromBlocks 0 0 (crossCoef P₁ Q₁ P₂ Q₂ mn)
(Matrix.kroneckerMap (· * ·) (P₁ mn.1) (P₂ mn.2))
end PolyAssembly