Forward matrix product

A forward matrix product packages a finite history of linear updates into one matrix. For a sequence of square matrices \(A_0,A_1,A_2,\ldots\), this project writes

when \(k\) is positive, and sets \(P_A(0)=I\). The convention is designed for column vectors. Starting from \(x_0=x\), the recurrence

gives \(x_k=P_A(k)x\). The earliest matrix acts first, even though it appears furthest to the right in the written product. The newest matrix acts last and therefore appears on the left.

That reversal between reading order and action order is the central fact to remember. It follows from composition, not from a typographical preference. Transition and fundamental matrices in finite-dimensional linear dynamics use the same chronological logic (Coppel).

The first four horizons

The safest way to learn the convention is to expand the first few cases:

Applied to a column vector \(x\), these become

The horizon \(k\) counts factors, not the largest time index. Thus \(P_A(3)\) uses the factors with indices \(0,1,2\). This zero-based convention matches the natural-number recursion used in Lean.

The empty product must be the identity. It makes the state at time zero equal to its initial value, makes concatenation valid when either block is empty, and makes a constant family agree with the zeroth matrix power.

The defining recursion

The project defines the product recursively:

def forwardProduct (A : ℕ → Matrix ι ι 𝕜) : ℕ → Matrix ι ι 𝕜
  | 0 => 1
  | k + 1 => A k * forwardProduct A k

The successor equation says to prepend the newest factor:

This direction matters because matrices generally do not commute. Replacing the right side by \(P_A(k)A_k\) would define a different product and would reverse chronological action on column vectors.

Only modest algebra is needed. The index type \(\iota\) is finite and has decidable equality so that matrix multiplication is a finite sum. The scalar type \(\mathbb K\) is a semiring, which supplies zero, one, addition, multiplication, distributivity, and associativity. The definition does not need subtraction, division, an order, a topology, a norm, or probability.

The index type may be empty. There is still one empty square matrix, and its identity and multiplication are well-defined. Empty dimension becomes a separate issue only when a normalized operator norm is requested.

Splitting a history after a chosen time

Let the first block contain \(m\) steps and the second contain \(k\) steps. Define the shifted sequence by

Then the checked split law is

The earlier block is on the right because it acts first. The later, shifted block is on the left because it acts second. For example, taking \(m=2\) and \(k=3\) gives

This is the discrete-time analogue of composing a transition from time zero to time \(m\) with a transition from time \(m\) to time \(m+k\). It is also the finite algebraic skeleton of a cocycle law. The current module does not define a base dynamical system or prove a random-cocycle theorem.

Constant systems recover powers

If every factor is the same matrix \(B\), the nonautonomous product reduces to an ordinary power:

The first cases agree:

If every factor is the identity, every forward product is the identity. These facts are calibration tests. They show that the time-dependent definition extends the familiar autonomous iteration \(x_{j+1}=Bx_j\).

A two-dimensional example where order matters

Consider

The first update shears the vector:

The second update stretches its first coordinate:

Accordingly, \(P_A(2)=A_1A_0\). Reversing the factors gives

which is different. A harmless-looking order reversal therefore changes the dynamics.

The checked Lean interface

forwardProduct A (k + 1) = A k * forwardProduct A k

The algebraic part of the module publishes nine declarations:

The last theorem uses Mathlib’s compatibility between matrix multiplication and matrix-vector multiplication, Matrix.mulVec_mulVec (Mathlib contributors). It turns the matrix recursion directly into the state recursion.

Type the noncommutative example locally

This worksheet models two-by-two integer matrices and column vectors with Std only. Save it as ForwardProductTutorial.lean:

import Std

structure Mat2 where
  a00 : Int
  a01 : Int
  a10 : Int
  a11 : Int
deriving Repr, DecidableEq

structure Vec2 where
  x0 : Int
  x1 : Int
deriving Repr, DecidableEq

def Mat2.mul (A B : Mat2) : Mat2 :=
  { a00 := A.a00 * B.a00 + A.a01 * B.a10
    a01 := A.a00 * B.a01 + A.a01 * B.a11
    a10 := A.a10 * B.a00 + A.a11 * B.a10
    a11 := A.a10 * B.a01 + A.a11 * B.a11 }

def Mat2.mulVec (A : Mat2) (x : Vec2) : Vec2 :=
  { x0 := A.a00 * x.x0 + A.a01 * x.x1
    x1 := A.a10 * x.x0 + A.a11 * x.x1 }

def shear : Mat2 :=
  { a00 := 1, a01 := 1, a10 := 0, a11 := 1 }

def stretch : Mat2 :=
  { a00 := 2, a01 := 0, a10 := 0, a11 := 1 }

def initial : Vec2 := { x0 := 0, x1 := 1 }

#eval shear.mulVec initial
#eval stretch.mulVec (shear.mulVec initial)
#eval shear.mulVec (stretch.mulVec initial)
#eval stretch.mul shear
#eval shear.mul stretch

example : stretch.mulVec (shear.mulVec initial) =
    { x0 := 2, x1 := 1 } := by decide
example : shear.mulVec (stretch.mulVec initial) =
    { x0 := 1, x1 := 1 } := by decide
example : stretch.mul shear ≠ shear.mul stretch := by decide

Run it with the installed pinned toolchain:

elan run leanprover/lean4:v4.32.0 lean ForwardProductTutorial.lean

The first three outputs are \((1,1)\), \((2,1)\), and \((1,1)\). The last two outputs are distinct matrix products. The kernel-certified examples then make both trajectories and noncommutativity explicit. This miniature checks the finite arithmetic and order convention, not Mathlib’s generic matrix API.

import NonlinearDynamics.Random.MatrixProducts.FiniteProducts

#check NonlinearDynamics.Random.MatrixProducts.forwardProduct
#check NonlinearDynamics.Random.MatrixProducts.forwardProduct_zero
#check NonlinearDynamics.Random.MatrixProducts.forwardProduct_succ
#check NonlinearDynamics.Random.MatrixProducts.forwardProduct_add
#check NonlinearDynamics.Random.MatrixProducts.forwardProduct_const
#check NonlinearDynamics.Random.MatrixProducts.forwardProduct_mulVec_succ

cd formalization
lake env lean -DwarningAsError=true NonlinearDynamics/Random/MatrixProducts/FiniteProducts.lean

What the definition does not say

The phrase forward product fixes an order and an empty-product convention. It does not by itself say that the factors are random, measurable, independent, stationary, invertible, or identically distributed. It does not supply a base flow, a cocycle over that flow, or an infinite product.

It also makes no growth claim. A product may expand some vectors, contract others, or alternate between both behaviors. The companion induced infinity operator norm entry explains one finite-horizon upper-bound mechanism. Such an upper bound is not automatically an equality, a sharp rate, a Lyapunov exponent, or a stability theorem.

In nonlinear dynamics, products of derivative matrices describe linearized perturbation propagation along an orbit. That application motivates the interface, but the present Lean module contains no differentiable map, no Jacobian identification, and no theorem connecting a nonlinear orbit to this matrix sequence.

Random products are another major destination. Oseledets’ multiplicative ergodic theorem classically organizes long-time exponential growth rates under substantial dynamical and integrability hypotheses (Oseledets). Nothing in the finite recursive definition proves those hypotheses or conclusions.

Exercises

1. Expand \(P_A(4)x\) with parentheses showing chronological action.
2. Check the split law for \(m=1\) and \(k=3\) by writing every factor.
3. Explain why \(P_A(m+k)=P_A(m)P_{A^{(m)}}(k)\) is generally false.
4. For the matrices in the worked example, compute both \(A_1A_0\) and \(A_0A_1\).
5. Prove on paper by induction that a constant family gives \(B^k\). Identify why the successor-power convention must match left multiplication.
6. Describe the unique forward product when the matrix index type is empty. Which parts of the algebraic interface still make sense?

Where to continue

Ordered Finite Matrix Products and Operator-Norm Growth develops all thirteen public declarations in the module, including the exact assumption ledger and finite-horizon product, power, and orbit bounds.

The next checked layer evaluates the factors at one outcome, proves exact finite-prefix measurability, and forms a pushforward law. Begin with the finite random-matrix product entry, then climb Measurable Finite Random-Matrix Products and Proof-Carrying Pushforward Laws.

Read the induced infinity operator norm entry before interpreting those bounds. The Hermitian Frobenius geometry entry explains a different, entrywise Euclidean matrix norm. The earlier Finite Product Probability Spaces and Independent Gaussian Fields uses product for a product probability measure. That commutative measure construction should not be confused with an ordered, generally noncommutative matrix product.

References

Mathlib contributors. Matrix-vector multiplication, Mathlib 4 documentation. This official interface supplies the compatibility between matrix multiplication and successive action on a column vector.

W. A. Coppel. Dichotomies in Stability Theory, Lecture Notes in Mathematics, Springer, 1978. This monograph supplies the classical stability motivation for transition matrices and products in linear evolution problems. The page’s exact indexing convention is fixed by the Lean definition above.

V. I. Oseledets. A multiplicative ergodic theorem. Characteristic Ljapunov exponents of dynamical systems, Transactions of the Moscow Mathematical Society 19 (1968), 197-231. This primary source identifies the long-time random-dynamical destination. Its ergodic hypotheses and asymptotic conclusions are not formalized in the finite-product module.

The exact upstream Lean source audited for this entry is Mathlib commit 81a5d257, the revision pinned by formalization/lake-manifest.json.