Traces and determinant pencils under rectangular congruence

For a rectangular matrix M, congruence A ↦ M * A * Mᵀ can be moved across a trace pairing or a determinant pencil det (1 + c • (B * _)) by congruating the test matrix B with the transpose instead. These identities transport Wishart trace transforms along congruence.

Main results

• Matrix.trace_mul_congruence — trace (B * (M * A * Mᵀ)) = trace ((Mᵀ * B * M) * A).
• Matrix.det_one_add_smul_transpose_mul_mul, Matrix.det_one_sub_smul_transpose_mul_mul — the corresponding determinant pencil identities, instances of the Weinstein--Aronszajn identity Matrix.det_one_add_mul_comm.
• Matrix.submatrix_one_mul_mul_submatrix_one — congruence by a selection matrix is the corresponding submatrix.

References

• R. J. Muirhead, Aspects of Multivariate Statistical Theory, Wiley, 1982, chapters 2–3.

theorem Matrix.trace_mul_congruence {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [NonUnitalCommSemiring R] (B : Matrix m m R) (M : Matrix m n R) (A : Matrix n n R) : (B * (M * A * M.transpose)).trace = (M.transpose * B * M * A).trace

Moving a rectangular congruence across a trace pairing transposes the congruence matrix. No symmetry hypotheses on A or B are needed.

theorem Matrix.det_one_add_smul_transpose_mul_mul {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing R] (c : R) (B : Matrix m m R) (M : Matrix m n R) (A : Matrix n n R) : (1 + c • (M.transpose * B * M * A)).det = (1 + c • (B * (M * A * M.transpose))).det

The Weinstein--Aronszajn identity in the form used by a rectangular congruence: the determinant pencil can be computed either before or after applying the congruence.

theorem Matrix.det_one_sub_smul_transpose_mul_mul {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing R] (c : R) (B : Matrix m m R) (M : Matrix m n R) (A : Matrix n n R) : (1 - c • (M.transpose * B * M * A)).det = (1 - c • (B * (M * A * M.transpose))).det

The subtractive form of Matrix.det_one_add_smul_transpose_mul_mul. This is the form of the determinant pencil occurring in Wishart moment-generating functions.

@[simp]

theorem Matrix.submatrix_one_mul_mul_submatrix_one {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype n] [DecidableEq n] [NonAssocSemiring R] (f : m → n) (A : Matrix n n R) : submatrix 1 f id * A * submatrix 1 id f = A.submatrix f f

Congruence by a selection matrix reads off a submatrix. The matrix (1 : Matrix n n R).submatrix f id keeps the rows named by f and its transpose (1 : Matrix n n R).submatrix id f keeps the columns, so congruating with it keeps exactly the rows and columns named by f.