High-contrast homogenization: Geometry.DetOrder

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Determinants and the Loewner order

The canonical block geometry takes determinants across Loewner inequalities twice. In the determinant bound for the canonical metric the balance chain M(E) ≤ E ≤ 𝔡(E)^{1/2} M(E) is read through the determinant, and in e.global.selection.metric.loss the product of the generalized eigenvalues of a pair is the quotient det(E)/det(F) of the two determinants. Both steps rest on the two facts collected here:

• the determinant is monotone for the Loewner order on positive definite data, and a matrix above the identity has determinant at least one;
• a matrix above the identity has spectral norm at most its determinant.

The last one is the scalar form of the reference text's sentence "every eigenvalue of F^{-1/2}EF^{-1/2} is at least one and their product is det(E)/det(F), so each eigenvalue is at most det(E)/det(F)": on positive data ‖·‖ is the largest eigenvalue, and the remaining eigenvalues contribute a factor at least one to the product.

All three statements are read off the eigenvalues of a symmetric matrix, so the file opens with the two facts about them that are used. An eigenvalue is the quadratic form evaluated at the corresponding unit eigenvector, which turns a Loewner hypothesis into a bound on every eigenvalue; conversely a matrix all of whose eigenvalues are at most t is bounded by t I, which is the spectral theorem read as a congruence of the diagonalization.

Eigenvalues of a symmetric matrix

theorem HCPolySupport.HighContrast.dotProduct_eigenvectorBasis_self {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.IsHermitian) (i : n) : star (hA.eigenvectorBasis i).ofLp ⬝ᵥ (hA.eigenvectorBasis i).ofLp = 1

The eigenvectors of a symmetric matrix are unit vectors for the dot product.

theorem HCPolySupport.HighContrast.one_le_eigenvalues_of_one_le {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.IsHermitian) (h : 1 ≤ A) (i : n) : 1 ≤ hA.eigenvalues i

A Loewner bound below is a bound on every eigenvalue. Evaluating the quadratic form of A - I at the i-th unit eigenvector gives eigenvalues A i - 1 ≥ 0.

theorem HCPolySupport.HighContrast.le_smul_one_of_eigenvalues_le {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.IsHermitian) {t : ℝ} (h : ∀ (i : n), hA.eigenvalues i ≤ t) : A ≤ t • 1

A bound on every eigenvalue is a Loewner bound above. This is the spectral theorem: the diagonalization is a congruence, and the diagonal matrix t I - diag(eigenvalues) has nonnegative entries.

Determinant monotonicity

theorem HCPolySupport.HighContrast.one_le_det_of_one_le {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.PosDef) (h : 1 ≤ A) : 1 ≤ A.det

A matrix above the identity has determinant at least one.

theorem HCPolySupport.HighContrast.norm_le_det_of_one_le {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.PosDef) (h : 1 ≤ A) : ‖A‖ ≤ A.det

A matrix above the identity has spectral norm at most its determinant. This is the scalar form of the eigenvalue argument of e.global.selection.metric.loss: the largest eigenvalue is at most the product of all of them, because the others are at least one.

theorem HCPolySupport.HighContrast.det_conj_matSqrt_inv {n : Type u_1} [Fintype n] [DecidableEq n] {A B : Matrix n n ℝ} (hA : A.PosDef) : (matSqrt A⁻¹ * B * matSqrt A⁻¹).det = B.det / A.det

The determinant of a normalization. Conjugating by A^{-1/2} divides the determinant by det A; this is the reference text's "their product is det(E)/det(F)".

theorem HCPolySupport.HighContrast.det_le_det_of_le {n : Type u_1} [Fintype n] [DecidableEq n] {A B : Matrix n n ℝ} (hA : A.PosDef) (hB : B.PosDef) (h : A ≤ B) : A.det ≤ B.det

The determinant is monotone for the Loewner order. Conjugating A ≤ B by A^{-1/2} gives I ≤ A^{-1/2} B A^{-1/2}, whose determinant is det(B)/det(A).

theorem HCPolySupport.HighContrast.relSize_le_det_div {n : Type u_1} [Fintype n] [DecidableEq n] {E F : Matrix n n ℝ} (hE : E.PosDef) (hF : F.PosDef) (h : F ≤ E) : relSize E F ≤ E.det / F.det

The determinant quotient bounds the relative size. This is the opening sentence of the proof of e.global.selection.metric.loss: if F ≤ E then every generalized eigenvalue of E relative to F is at least one, so the largest of them — the relative size — is at most their product det(E)/det(F). No eigenvalue is named: the largest one is ‖F^{-1/2} E F^{-1/2}‖ and the product is its determinant.