Sandwiches by the square root of a positive-semidefinite matrix

The continuous-functional-calculus square root CFC.sqrt S of a matrix S is positive semidefinite (CFC.sqrt_nonneg), hence Hermitian. Sandwiching a Hermitian matrix Θ between two copies of it gives the Hermitian matrix CFC.sqrt S * Θ * CFC.sqrt S, whose quadratic form is the pullback of the quadratic form of Θ along CFC.sqrt S. For positive-semidefinite S, its pencils 1 - c • (CFC.sqrt S * Θ * CFC.sqrt S) have the same determinant as those of Θ * S, by Sylvester's determinant identity and CFC.sqrt S * CFC.sqrt S = S; by cyclicity, the sandwich and its square also have the same traces as Θ * S and Θ * S * Θ * S.

Over the reals the square root is symmetric, so for a positive-definite T the identity CFC.sqrt T * CFC.sqrt T = T exhibits T as C * Cᵀ with C invertible.

The sandwich is the matrix whose eigenvalues govern the exponential moments of a Gaussian quadratic form, and the determinant identity is what turns its spectral formula into a formula in the original parameters.

When S is positive definite the same pencil has a scale form: for any X, the matrix S⁻¹ - X is the congruence of 1 - CFC.sqrt S * X * CFC.sqrt S by (CFC.sqrt S)⁻¹, so the two are positive definite together. Taking X to be a scaled matrix c • Θ gives the form that appears in an exponential weight exp (-trace ((S⁻¹ - c • Θ) * A) / 2), where S is a scale matrix and c • Θ the tilt of a trace statistic. Its determinant needs no positivity at all, and is computed over a commutative ring in TauCeti/LinearAlgebra/Matrix/InvSub.lean.

Main results

• Matrix.isHermitian_sqrt_mul_mul_sqrt — the sandwich of a Hermitian matrix by a square root is Hermitian;
• Matrix.PosSemidef.rank_sqrt — the square root of a positive-semidefinite matrix has the same rank;
• Matrix.inner_toEuclideanCLM_sqrt_toEuclideanLin — the quadratic form of Θ at CFC.sqrt S x is the quadratic form of the sandwich at x;
• Matrix.PosSemidef.det_one_sub_smul_sqrt_mul_mul_sqrt_eq_det_one_sub_smul_mul — for positive-semidefinite S, the pencil determinants of the sandwich and of Θ * S agree;
• Matrix.PosSemidef.trace_sqrt_mul_mul_sqrt and Matrix.PosSemidef.trace_sqrt_mul_mul_sqrt_mul_self — for positive-semidefinite S, the traces of the sandwich and of its square are those of Θ * S and Θ * S * Θ * S;
• Matrix.PosDef.inv_sub_eq_conjugate and Matrix.PosDef.posDef_inv_sub_iff — the scale form S⁻¹ - X of the pencil and its positive-definiteness;
• Matrix.PosDef.inv_sub_smul_eq_conjugate and Matrix.PosDef.posDef_inv_sub_smul_iff — the same two statements for a scaled perturbation c • Θ;
• Matrix.PosDef.exists_generalLinearGroup_mul_transpose_eq — every positive-definite real matrix is C * Cᵀ for an invertible C.

@[simp]

theorem Matrix.PosSemidef.rank_sqrt {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] {S : Matrix ι ι 𝕜} (hS : S.PosSemidef) : (CFC.sqrt S).rank = S.rank

The square root of a positive-semidefinite matrix has the same rank as the matrix.

theorem Matrix.isHermitian_sqrt_mul_mul_sqrt {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] (S : Matrix ι ι 𝕜) {Θ : Matrix ι ι 𝕜} (hΘ : Θ.IsHermitian) : (CFC.sqrt S * Θ * CFC.sqrt S).IsHermitian

Sandwiching a Hermitian matrix between two copies of a square root gives a Hermitian matrix.

theorem Matrix.inner_toEuclideanCLM_sqrt_toEuclideanLin {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (S Θ : Matrix ι ι 𝕜) (x : EuclideanSpace 𝕜 ι) : inner 𝕜 ((toEuclideanCLM (CFC.sqrt S)) x) ((toEuclideanLin Θ) ((toEuclideanCLM (CFC.sqrt S)) x)) = inner 𝕜 x ((toEuclideanLin (CFC.sqrt S * Θ * CFC.sqrt S)) x)

The quadratic form of Θ at CFC.sqrt S x is the quadratic form of the sandwich CFC.sqrt S * Θ * CFC.sqrt S at x.

theorem Matrix.PosSemidef.det_one_sub_smul_sqrt_mul_mul_sqrt_eq_det_one_sub_smul_mul {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {S : Matrix ι ι 𝕜} (hS : S.PosSemidef) (Θ : Matrix ι ι 𝕜) (c : 𝕜) : (1 - c • (CFC.sqrt S * Θ * CFC.sqrt S)).det = (1 - c • (Θ * S)).det

For positive-semidefinite S, the pencils of the sandwich CFC.sqrt S * Θ * CFC.sqrt S and of the product Θ * S have the same determinant.

theorem Matrix.PosSemidef.trace_sqrt_mul_mul_sqrt {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] {S : Matrix ι ι 𝕜} (hS : S.PosSemidef) (M : Matrix ι ι 𝕜) : (CFC.sqrt S * M * CFC.sqrt S).trace = (M * S).trace

For positive-semidefinite S, the trace of the sandwich CFC.sqrt S * M * CFC.sqrt S is the trace of M * S.

theorem Matrix.PosSemidef.trace_sqrt_mul_mul_sqrt_mul_self {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] {S : Matrix ι ι 𝕜} (hS : S.PosSemidef) (M : Matrix ι ι 𝕜) : (CFC.sqrt S * M * CFC.sqrt S * (CFC.sqrt S * M * CFC.sqrt S)).trace = (M * S * M * S).trace

For positive-semidefinite S, the trace of the square of the sandwich CFC.sqrt S * M * CFC.sqrt S is the trace of M * S * M * S.

The scale form of the pencil

theorem Matrix.PosDef.inv_sub_eq_conjugate {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {S : Matrix ι ι 𝕜} (hS : S.PosDef) (X : Matrix ι ι 𝕜) : S⁻¹ - X = (CFC.sqrt S)⁻¹ * (1 - CFC.sqrt S * X * CFC.sqrt S) * (CFC.sqrt S)⁻¹

The scale form of the pencil. For positive-definite S and any X, the matrix S⁻¹ - X is the congruence of the sandwich pencil 1 - CFC.sqrt S * X * CFC.sqrt S by (CFC.sqrt S)⁻¹.

theorem Matrix.PosDef.posDef_inv_sub_iff {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {S : Matrix ι ι 𝕜} (hS : S.PosDef) (X : Matrix ι ι 𝕜) : (S⁻¹ - X).PosDef ↔ (1 - CFC.sqrt S * X * CFC.sqrt S).PosDef

The scale pencil S⁻¹ - X is positive definite exactly when the sandwich pencil 1 - CFC.sqrt S * X * CFC.sqrt S is. X needs no hypothesis: congruence by the invertible Hermitian matrix (CFC.sqrt S)⁻¹ transports positive definiteness in both directions.

theorem Matrix.PosDef.inv_sub_smul_eq_conjugate {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {S : Matrix ι ι 𝕜} (hS : S.PosDef) (Θ : Matrix ι ι 𝕜) (c : 𝕜) : S⁻¹ - c • Θ = (CFC.sqrt S)⁻¹ * (1 - c • (CFC.sqrt S * Θ * CFC.sqrt S)) * (CFC.sqrt S)⁻¹

The scale form of the pencil, for a scaled perturbation: S⁻¹ - c • Θ is the congruence of 1 - c • (CFC.sqrt S * Θ * CFC.sqrt S) by (CFC.sqrt S)⁻¹.

theorem Matrix.PosDef.posDef_inv_sub_smul_iff {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {S : Matrix ι ι 𝕜} (hS : S.PosDef) (Θ : Matrix ι ι 𝕜) (c : 𝕜) : (S⁻¹ - c • Θ).PosDef ↔ (1 - c • (CFC.sqrt S * Θ * CFC.sqrt S)).PosDef

The scale pencil S⁻¹ - c • Θ is positive definite exactly when the sandwich pencil 1 - c • (CFC.sqrt S * Θ * CFC.sqrt S) is. Neither Θ nor c needs a hypothesis.

The square-root factorization over the reals

theorem Matrix.PosDef.exists_generalLinearGroup_mul_transpose_eq {ι : Type u_2} [Fintype ι] [DecidableEq ι] {T : Matrix ι ι ℝ} (hT : T.PosDef) : ∃ (C : GL ι ℝ), ↑C * (↑C).transpose = T

Every positive-definite real matrix is C * Cᵀ for an invertible C, namely its square root, which is symmetric. Congruence by that C is what absorbs a positive-definite scale matrix into the positive-definite cone.