The entries of a matrix power as a sum over paths

Category: 1-Mathlib (CSD-free; staged for upstream).

An entry of M ^ n is a sum over all index paths of n steps from the row to the column index, each path weighted by the product of the entries it traverses. Mathlib carries this only for adjacency matrices, as a count of walks (SimpleGraph.adjMatrix_pow_apply_eq_card_walk); this file is the weighted form over a commutative semiring, in the shape the sum-over-paths reading of a matrix exponential needs: the row and column indices fixed, the sum over the intermediate states.

• Matrix.pathWeight M p — the weight of the path p : Fin (n + 1) → ι, the product ∏ k, M (p k) (p (k + 1)) of the entries along its n steps;
• Matrix.pathWeight_cons — prepending a state multiplies the weight by the entry of the new first step;
• ★ Matrix.pow_succ_apply_eq_sum_pathWeight — the sum over paths: (M ^ (n + 1)) i j = ∑ p : Fin n → ι, pathWeight M (Fin.cons i (Fin.snoc p j)), the sum over every choice of the n intermediate states of the path from i to j in n + 1 steps.

Honest scope

⚠️ Commutative scalars. The weight of a path is a Finset product, so the scalars are a CommSemiring; over a noncommutative ring the product along a path is ordered and would be a List.prod. The consumer (Analysis/Matrix/SumOverPaths.lean) works over ℂ.

References: Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean (adjMatrix_pow_apply_eq_card_walk, the unweighted case); consumer Analysis/Matrix/SumOverPaths.lean; specs/future-work.md, specs/BACKLOG.md #36.

def Matrix.pathWeight {ι : Type u_1} {R : Type u_2} [CommSemiring R] (M : Matrix ι ι R) {n : ℕ} (p : Fin (n + 1) → ι) : R

The weight of an n-step path p through the index set, for the matrix M: the product of the entries of M along the steps of p.

Equations

• M.pathWeight p = ∏ k : Fin n, M (p k.castSucc) (p k.succ)

theorem Matrix.pathWeight_def {ι : Type u_1} {R : Type u_2} [CommSemiring R] (M : Matrix ι ι R) {n : ℕ} (p : Fin (n + 1) → ι) : M.pathWeight p = ∏ k : Fin n, M (p k.castSucc) (p k.succ)

pathWeight, unfolded.

@[simp]

theorem Matrix.pathWeight_zero {ι : Type u_1} {R : Type u_2} [CommSemiring R] (M : Matrix ι ι R) (p : Fin 1 → ι) : M.pathWeight p = 1

A path with no steps has weight one.

theorem Matrix.pathWeight_one {ι : Type u_1} {R : Type u_2} [CommSemiring R] (M : Matrix ι ι R) (p : Fin 2 → ι) : M.pathWeight p = M (p 0) (p 1)

A one-step path has the weight of its one entry.

theorem Matrix.pathWeight_cons {ι : Type u_1} {R : Type u_2} [CommSemiring R] (M : Matrix ι ι R) {n : ℕ} (i : ι) (q : Fin (n + 1) → ι) : M.pathWeight (Fin.cons i q) = M i (q 0) * M.pathWeight q

Prepending a state i to a path q multiplies the weight by the entry of the new first step, from i to the first state of q.

theorem Matrix.pow_succ_apply_eq_sum_pathWeight {ι : Type u_1} {R : Type u_2} [Fintype ι] [DecidableEq ι] [CommSemiring R] (M : Matrix ι ι R) (n : ℕ) (i j : ι) : (M ^ (n + 1)) i j = ∑ p : Fin n → ι, M.pathWeight (Fin.cons i (Fin.snoc p j))

★ The entries of a matrix power are sums over paths. The (i, j) entry of M ^ (n + 1) is the sum, over every choice p of the n intermediate states, of the weight of the path i, p 0, …, p (n - 1), j.