Documentation

Reconstruction.Newton

Newton's Identities for Matrices #

Newton's identities (Faddeev–LeVerrier recurrence) relate the traces of powers of a matrix to the coefficients of its characteristic polynomial.

Main results #

Proof outline #

From Cayley–Hamilton #

The Cayley–Hamilton theorem (Matrix.aeval_self_charpoly) gives p(A) = 0 where p(x) = x^n + c_{n-1} x^{n-1} + ⋯ + c_1 x + c_0 is the characteristic polynomial.

Taking the trace of p(A) = 0: ∑_{i=0}^{n} c_i · tr(A^i) = 0

Since c_n = 1 (monic) and tr(A^0) = tr(I) = n: tr(A^n) + c_{n-1} tr(A^{n-1}) + ⋯ + c_1 tr(A) + c_0 · n = 0

This determines c_0 from the traces and higher coefficients.

For k < n, Newton's identities follow from differentiating det(xI - A) and applying the product rule to the Leibniz expansion.

References #

theorem Matrix.newton_trace_charpoly {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [CommRing R] (A : Matrix n n R) {k : } (hk : 1 k) (hk' : k Fintype.card n) :
(A ^ k).trace + jFinset.range (k - 1), A.charpoly.coeff (Fintype.card n - (j + 1)) * (A ^ (k - (j + 1))).trace + k * A.charpoly.coeff (Fintype.card n - k) = 0

Newton's identity at step k. For a matrix A over a commutative ring and 1 ≤ k ≤ |n|:

tr(A^k) + ∑_{j=1}^{k-1} c_{|n|-j} · tr(A^{k-j}) + k · c_{|n|-k} = 0

where c_i denotes A.charpoly.coeff i.

The full set of Newton identities for k = 1, ..., |n| determines all coefficients of the characteristic polynomial from the traces of powers, and vice versa.

theorem Matrix.cayley_hamilton_trace {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [CommRing R] (A : Matrix n n R) :
iFinset.range (Fintype.card n + 1), A.charpoly.coeff i * (A ^ i).trace = 0

Cayley–Hamilton trace identity. Taking the trace of p(A) = 0 (Cayley–Hamilton) yields a linear relation among c_i · tr(A^i):

∑_{i=0}^{n} charpoly.coeff(i) · tr(A^i) = 0

Since charpoly is monic of degree n, the coefficient of x^n is 1, so this is equivalent to:

tr(A^n) + ∑_{i=0}^{n-1} c_i · tr(A^i) = 0

At i = 0: tr(A^0) = tr(I) = n, so the c_0 term contributes n · c_0. This determines c_0 from tr(A), ..., tr(A^n) and c_1, ..., c_{n-1}.