Eigen-coordinates of a Hermitian matrix

Let B be a Hermitian matrix over an RCLike field with orthonormal eigenvector basis hB.eigenvectorBasis and real eigenvalues hB.eigenvalues. This file reads three quantities off the eigen-coordinates: the quadratic form x ↦ ⟪x, B x⟫, which becomes a weighted sum of squared moduli, and the diagonalization and the determinant of the pencil 1 - c • B, which are read off the scalars 1 - c * hB.eigenvalues j. The pencil is diagonal in the eigenbasis for any scalar c; only its positive definiteness asks for a real one.

These are the spectral facts behind the moment-generating function of a Gaussian quadratic form, whose exponential-integrability domain is a positive-definiteness condition on such a pencil and whose value is a power of its determinant.

Main results

• Matrix.IsHermitian.inner_toEuclideanLin_sum_smul_eigenvectorBasis — the quadratic form of B at ∑ j, c j • b j is ∑ j, hB.eigenvalues j * ‖c j‖ ^ 2;
• Matrix.IsHermitian.posDef_one_sub_smul_iff — 1 - c • B is positive definite exactly when c * hB.eigenvalues j < 1 for every j;
• Matrix.IsHermitian.one_sub_smul_eq_conjStarAlgAut_diagonal and Matrix.IsHermitian.det_one_sub_smul — 1 - c • B is conjugate to a diagonal matrix, and its determinant is ∏ j, (1 - c * hB.eigenvalues j).

theorem Matrix.IsHermitian.inner_toEuclideanLin_sum_smul_eigenvectorBasis {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {B : Matrix ι ι 𝕜} (hB : B.IsHermitian) (c : ι → 𝕜) : inner 𝕜 (∑ j : ι, c j • hB.eigenvectorBasis j) ((toEuclideanLin B) (∑ j : ι, c j • hB.eigenvectorBasis j)) = ∑ j : ι, ↑(hB.eigenvalues j) * ↑‖c j‖ ^ 2

In the eigen-coordinates of a Hermitian matrix, its quadratic form is the sum of the squared moduli of the coordinates weighted by the eigenvalues.

theorem Matrix.IsHermitian.one_sub_smul_eq_conjStarAlgAut_diagonal {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {B : Matrix ι ι 𝕜} (hB : B.IsHermitian) (c : 𝕜) : 1 - c • B = ((Unitary.conjStarAlgAut 𝕜 (Matrix ι ι 𝕜)) hB.eigenvectorUnitary) (diagonal fun (j : ι) => 1 - c * ↑(hB.eigenvalues j))

The pencil 1 - c • B is conjugate, by the eigenvector unitary of B, to the diagonal matrix with entries 1 - c * hB.eigenvalues j.

theorem Matrix.IsHermitian.posDef_one_sub_smul_iff {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {B : Matrix ι ι 𝕜} (hB : B.IsHermitian) (c : ℝ) : (1 - c • B).PosDef ↔ ∀ (j : ι), c * hB.eigenvalues j < 1

The pencil 1 - c • B is positive definite exactly when c * hB.eigenvalues j < 1 for every eigenvalue.

theorem Matrix.IsHermitian.det_one_sub_smul {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {B : Matrix ι ι 𝕜} (hB : B.IsHermitian) (c : 𝕜) : (1 - c • B).det = ∏ j : ι, (1 - c * ↑(hB.eigenvalues j))

The determinant of the pencil 1 - c • B is the product of 1 - c * hB.eigenvalues j over the eigenvalues.