Entries of a product of matrices as a sum over paths

The entry (a, b) of a product M 0 * M 1 * ⋯ * M (d - 1) of square matrices is the sum, over all paths p 0, p 1, …, p d of indices from p 0 = a to p d = b, of the products ∏ i, M i (p i) (p (i + 1)) of the entries along the path. This is the standard expansion behind algebraic branching programs.

Main results

• Matrix.list_prod_ofFn_apply: the path expansion of an entry of (List.ofFn M).prod.

theorem Matrix.list_prod_ofFn_apply {ι : Type u_1} {R : Type u_2} [Fintype ι] [DecidableEq ι] [CommSemiring R] {d : ℕ} (M : Fin d → Matrix ι ι R) (a b : ι) : (List.ofFn M).prod a b = ∑ p : Fin (d + 1) → ι, if p 0 = a ∧ p (Fin.last d) = b then ∏ i : Fin d, M i (p i.castSucc) (p i.succ) else 0

The path expansion: the entry (a, b) of the product of the matrices M 0, …, M (d - 1) is the sum, over the paths p : Fin (d + 1) → ι from a to b, of the product of the entries M i (p i) (p (i + 1)) along the path.