The determinant of the pencil S⁻¹ - X

For an invertible square matrix S over a commutative ring and any X, the determinant of the pencil S⁻¹ - X is expressible in S and X themselves: multiplying through by det S clears the inverse, and Sylvester's determinant identity turns what is left into det (1 - X * S). The determinant of the inverse pencil follows, once the pencil is itself invertible.

Nothing here needs an order or a norm on the ring. Writing the perturbation as a scaled matrix c • Θ gives the scale form of the matrix pencil carried by an exponential weight exp (-trace ((S⁻¹ - c • Θ) * A) / 2), where S is a scale matrix and c • Θ the tilt of a trace statistic; the positivity of that form, which does need an order, is in TauCeti/Analysis/Matrix/Sqrt.lean.

Main results

• Matrix.det_mul_det_inv_sub — the determinant of the pencil, in the parameters S and X;
• Matrix.det_nonsing_inv_inv_sub — the determinant of the inverse pencil;
• Matrix.det_mul_det_inv_sub_smul and Matrix.det_nonsing_inv_inv_sub_smul — the same two identities for a scaled perturbation c • Θ.

theorem Matrix.det_mul_det_inv_sub {ι : Type u_1} [Fintype ι] [DecidableEq ι] {R : Type u_2} [CommRing R] {S : Matrix ι ι R} (hS : IsUnit S.det) (X : Matrix ι ι R) : S.det * (S⁻¹ - X).det = (1 - X * S).det

The determinant of the pencil S⁻¹ - X, in the parameters S and X themselves. Only the invertibility of S is used.

theorem Matrix.det_nonsing_inv_inv_sub {ι : Type u_1} [Fintype ι] [DecidableEq ι] {R : Type u_2} [CommRing R] {S : Matrix ι ι R} (hS : IsUnit S.det) {X : Matrix ι ι R} (hX : IsUnit (S⁻¹ - X).det) : (S⁻¹ - X)⁻¹.det = S.det * Ring.inverse (1 - X * S).det

The determinant of the inverse pencil (S⁻¹ - X)⁻¹.

theorem Matrix.det_mul_det_inv_sub_smul {ι : Type u_1} [Fintype ι] [DecidableEq ι] {R : Type u_2} [CommRing R] {S : Matrix ι ι R} (hS : IsUnit S.det) (Θ : Matrix ι ι R) (c : R) : S.det * (S⁻¹ - c • Θ).det = (1 - c • (Θ * S)).det

The determinant of the scale pencil S⁻¹ - c • Θ, in the parameters S and Θ themselves.

theorem Matrix.det_nonsing_inv_inv_sub_smul {ι : Type u_1} [Fintype ι] [DecidableEq ι] {R : Type u_2} [CommRing R] {S : Matrix ι ι R} (hS : IsUnit S.det) {Θ : Matrix ι ι R} {c : R} (hc : IsUnit (S⁻¹ - c • Θ).det) : (S⁻¹ - c • Θ)⁻¹.det = S.det * Ring.inverse (1 - c • (Θ * S)).det

The determinant of the inverse scale pencil. This is the determinant of the scale matrix carried by an exponential weight exp (-trace ((S⁻¹ - c • Θ) * A) / 2).