Newton's identities for traces of matrix powers

TheoremTraces of powers of a \(2 \times 2\) matrix#●ready to prove

Let \(M\) be a real \(2 \times 2\) matrix and let \(m \ge 1\) be an integer. Then

\[\operatorname{tr}(M^{2m}) = 2m \sum_{r=0}^{m} (-1)^r \frac{(2m - r - 1)!}{r! \, (2m - 2r)!} (\det M)^r (\operatorname{tr} M)^{2m - 2r}\]

and

\[\operatorname{tr}(M^{2m+1}) = (2m + 1) \sum_{r=0}^{m} (-1)^r \frac{(2m - r)!}{r! \, (2m + 1 - 2r)!} (\det M)^r (\operatorname{tr} M)^{2m + 1 - 2r}.\]

MathlibExt.LinearAlgebra.PowerSumMatrixWanted.trace_pow_two · 16 lines

theorem_wanted trace_pow_two (M : Matrix (Fin 2) (Fin 2) ℝ)
    (m : ℕ) (hm : 1 ≤ m) :
    Matrix.trace (M ^ (2 * m)) =
        (2 * m : ℝ) * ∑ r ∈ Finset.range (m + 1),
          (-1 : ℝ) ^ r *
            ((Nat.factorial (2 * m - r - 1) : ℝ) /
              ((Nat.factorial r : ℝ) *
                (Nat.factorial (2 * m - 2 * r) : ℝ))) *
            M.det ^ r * Matrix.trace M ^ (2 * m - 2 * r) ∧
      Matrix.trace (M ^ (2 * m + 1)) =
        (2 * m + 1 : ℝ) * ∑ r ∈ Finset.range (m + 1),
          (-1 : ℝ) ^ r *
            ((Nat.factorial (2 * m - r) : ℝ) /
              ((Nat.factorial r : ℝ) *
                (Nat.factorial (2 * m + 1 - 2 * r) : ℝ))) *
            M.det ^ r * Matrix.trace M ^ (2 * m + 1 - 2 * r)

Sources

• Peiran Ding, Yanjun Zhu and Lei Wang, "A New Formula for the Sum of Integer Powers Based on Elementary Matrix Theory", Theorem 1, equations (5) and (6).

TheoremIntegral of \(x^r (1 - x)^r\) over \((0, 1)\)#●ready to prove

For every natural number \(r\) (including \(r = 0\)),

\[\int_0^1 x^r (1 - x)^r \, dx = \frac{1}{(2r + 1) \binom{2r}{r}}.\]

theorem_wanted integral_pow_one_sub_pow (r : ℕ) :
    (∫ x in (0 : ℝ)..1, x ^ r * (1 - x) ^ r) =
      1 / ((2 * r + 1 : ℝ) * (Nat.choose (2 * r) r : ℝ))

Sources

• Peiran Ding, Yanjun Zhu and Lei Wang, "A New Formula for the Sum of Integer Powers Based on Elementary Matrix Theory", Lemma 3.

DefinitionCharacteristic-polynomial coefficients in descending order#✓fully proved

Let \(A\) be a square matrix over a commutative ring \(R\) whose rows and columns are indexed by a finite set of size \(N\), and write its characteristic polynomial as \(\chi_A(X) = \det(X I - A) = X^N + c_1 X^{N-1} + \dots + c_N\). For a natural number \(k\), the descending coefficient \(c_k\) of \(A\) is the coefficient of \(X^{N-k}\) in \(\chi_A\) when \(k \le N\), and \(0\) when \(k > N\).

Setting \(c_k = 0\) for \(k > N\) lets the trace recurrence be stated uniformly for all positive \(k\).

noncomputable def charpolyDescendingCoeff {R : Type*} [CommRing R]
    (A : Matrix n n R) (k : ℕ) : R :=
  if k ≤ Fintype.card n then
    Polynomial.coeff A.charpoly (Fintype.card n - k)
  else
    0

Used by 1

Used byNewton's trace identities for the characteristic polynomial

TheoremNewton's trace identities for the characteristic polynomial#●ready to prove

Let \(A\) be a square matrix over a commutative ring \(R\) whose rows and columns are indexed by a finite set of size \(N\). For each natural number \(k\), let \(c_k\) be the coefficient of \(X^{N-k}\) in the characteristic polynomial \(\chi_A(X) = \det(X I - A)\) when \(k \le N\), and \(c_k = 0\) when \(k > N\), so that \(\chi_A(X) = X^N + c_1 X^{N-1} + \dots + c_N\). Then for every natural number \(k \ge 1\),

\[k \, c_k + \sum_{j=1}^{k} \operatorname{tr}(A^j) \, c_{k-j} = 0,\]

where \(k\) is read as an element of \(R\).

public theorem_wanted trace_cayley_hamilton_newton {R : Type*} [CommRing R]
    (A : Matrix n n R) {k : ℕ} (hk : 1 ≤ k) :
    (k : R) * charpolyDescendingCoeff A k +
        ∑ j ∈ Finset.Icc 1 k,
          trace (A ^ j) * charpolyDescendingCoeff A (k - j) = 0

Sources

• Knill, Some fundamental theorems in mathematics, §220. Problem trace_cayley_hamilton_newton of the lean-eval benchmark.

Uses 1

Statement usesCharacteristic-polynomial coefficients in descending order

1 fully proved3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.