The positive semidefinite solution of A * S * A = T

The Loewner order on square matrices makes Matrix n n 𝕜 an algebra with a continuous functional calculus, so TauCeti.geometricMean applies to it: for S positive definite and T positive semidefinite there is exactly one positive semidefinite A with A * S * A = T, namely TauCeti.geometricMean S⁻¹ʳ T, which is the classical matrix √(S⁻¹) * √(√S * T * √S) * √(S⁻¹).

Read through covariance matrices, that matrix is the linear map pushing a centred Gaussian law of covariance S forward to one of covariance T, that is, the Brenier map between two Gaussians.

The solution is Hermitian, so for positive definite S and positive semidefinite T it solves the congruence equation A * S * Aᴴ = T as well; when T is positive definite the solution is positive definite itself, and its inverse is the solution TauCeti.geometricMean T⁻¹ʳ S of the reversed equation.

Main results

• Matrix.PosDef.existsUnique_posSemidef_mul_mul: existence and uniqueness of that matrix.
• Matrix.PosDef.geometricMean_ringInverse_eq_sqrt_mul_mul_sqrt: that matrix is the congruence (√S)⁻¹ * √(√S * T * √S) * (√S)⁻¹ of the positive square root of √S * T * √S.
• Matrix.isHermitian_geometricMean and Matrix.PosDef.posDef_geometricMean_ringInverse: the geometric mean is Hermitian, and this one is positive definite when T is.
• Matrix.PosDef.mul_mul_conjTranspose_geometricMean: the solution satisfies A * S * Aᴴ = T.
• Matrix.PosDef.inv_geometricMean_ringInverse: reversing S and T inverts the solution.
• Matrix.PosDef.trace_geometricMean_ringInverse_mul: the cross trace of the solution is the trace of the square root of the covariance sandwich.
• Matrix.PosDef.trace_one_sub_geometricMean_ringInverse_mul_mul_conjTranspose: the trace of the covariance left by subtracting the standard positive map.

theorem Matrix.PosDef.existsUnique_posSemidef_mul_mul {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] {S T : Matrix n n 𝕜} (hS : S.PosDef) (hT : T.PosSemidef) : ∃! A : Matrix n n 𝕜, A.PosSemidef ∧ A * S * A = T

For a positive definite S and a positive semidefinite T there is exactly one positive semidefinite matrix A with A * S * A = T; it is TauCeti.geometricMean S⁻¹ʳ T.

The standard positive matrix, its Hermitian symmetry, and its inverse

theorem Matrix.PosDef.geometricMean_ringInverse_eq_sqrt_mul_mul_sqrt {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] {S T : Matrix n n 𝕜} [DecidableEq n] (hS : S.PosDef) : TauCeti.geometricMean (Ring.inverse S) T = (CFC.sqrt S)⁻¹ * CFC.sqrt (CFC.sqrt S * T * CFC.sqrt S) * (CFC.sqrt S)⁻¹

The standard positive matrix. For a positive-definite S the matrix geometricMean S⁻¹ʳ T is the congruence (√S)⁻¹ * √(√S * T * √S) * (√S)⁻¹ of the positive square root of √S * T * √S by the inverse (√S)⁻¹ of the positive square root of S; when T is positive semidefinite it is the solution A of A * S * A = T.

theorem Matrix.isHermitian_geometricMean {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {a b : Matrix n n 𝕜} : (TauCeti.geometricMean a b).IsHermitian

The solution is Hermitian. The geometric mean √a * √(√a⁻¹ * b * √a⁻¹) * √a is a Hermitian matrix sandwiched between two copies of a Hermitian matrix: each square root is nonnegative, hence Hermitian. No positivity hypothesis is needed, so this is a statement about geometricMean a b for every a and b; in particular the solution A of A * S * A = T is Hermitian whenever S is positive definite and T is positive semidefinite.

theorem Matrix.PosDef.posDef_geometricMean_ringInverse {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] {S T : Matrix n n 𝕜} [DecidableEq n] (hS : S.PosDef) (hT : T.PosDef) : (TauCeti.geometricMean (Ring.inverse S) T).PosDef

The standard positive matrix of two positive-definite matrices is positive definite: the geometric mean of a strictly positive and of a strictly positive element is strictly positive.

@[simp]

theorem Matrix.PosDef.mul_mul_conjTranspose_geometricMean {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] {S T : Matrix n n 𝕜} [DecidableEq n] (hS : S.PosDef) (hT : T.PosSemidef) : TauCeti.geometricMean (Ring.inverse S) T * S * (TauCeti.geometricMean (Ring.inverse S) T).conjTranspose = T

The congruence form. The solution A of A * S * A = T for positive-definite S and positive-semidefinite T is Hermitian by isHermitian_geometricMean, so it solves the congruence A * S * Aᴴ = T as well. This is the form in which a covariance matrix transforms under a change of variables; over the reals Aᴴ is the transpose Aᵀ.

theorem Matrix.PosDef.trace_geometricMean_ringInverse_mul {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] {S T : Matrix n n 𝕜} [DecidableEq n] (hS : S.PosDef) : (TauCeti.geometricMean (Ring.inverse S) T * S).trace = (CFC.sqrt (CFC.sqrt S * T * CFC.sqrt S)).trace

An algebraic trace identity for geometricMean S⁻¹ʳ T. When T is positive semidefinite, the geometric mean is the standard positive solution and the right-hand side is the trace of the positive square root of the covariance sandwich.

theorem Matrix.PosDef.trace_one_sub_geometricMean_ringInverse_mul_mul_conjTranspose {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] {S T : Matrix n n 𝕜} [DecidableEq n] (hS : S.PosDef) (hT : T.PosSemidef) : ((1 - TauCeti.geometricMean (Ring.inverse S) T) * S * (1 - TauCeti.geometricMean (Ring.inverse S) T).conjTranspose).trace = S.trace + T.trace - 2 * (CFC.sqrt (CFC.sqrt S * T * CFC.sqrt S)).trace

The trace of the covariance transformed by 1 - A, for the standard positive solution A * S * A = T, is the Bures covariance expression.

@[simp]

theorem Matrix.PosDef.inv_geometricMean_ringInverse {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] {S T : Matrix n n 𝕜} [DecidableEq n] (hS : S.PosDef) (hT : T.PosDef) : (TauCeti.geometricMean (Ring.inverse S) T)⁻¹ = TauCeti.geometricMean (Ring.inverse T) S

Reversing the equation inverts the solution. The solution of A * S * A = T, inverted, is the solution of B * T * B = S: the geometric mean commutes with inversion and is symmetric in its two arguments.