High-contrast homogenization: Geometry.RelativeSize

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

The relative size of one positive matrix against another

The generalized eigenvalue functional Λ(F;E) = |F^{-1/2} E F^{-1/2}| of the reference text — it appears as the reference imbalance κ_ref of the entry comparison, and as the imbalance 𝔡 of e.response.canonical.imbalance — is written here as

relSize E F = ‖matSqrt F⁻¹ * E * matSqrt F⁻¹‖,

so that the numerator is the first argument and the denominator the second.

The whole file rests on one observation: conjugation by F^{-1/2} is a congruence that sends F to the identity, so a Loewner comparison E ≤ t F becomes a comparison against t I, which the spectral norm reads off exactly. The resulting characterization

relSize E F ≤ t ↔ E ≤ t • F        (`relSize_le_iff`, for `0 ≤ t`)

says that relSize E F is the least scalar t with E ≤ t F. Every other statement below is a formal consequence of it, including the invariance under a common congruence

relSize (Cᴴ E C) (Cᴴ F C) = relSize E F   (`relSize_congr`),

which is the "generalized eigenvalues are unchanged under a common congruence" step of the canonical balance.

The relative size of a positive definite matrix against itself is ‖1‖, which is 1 exactly when the index type is nonempty; the few statements that need that normalization carry a Nonempty instance.

Scalar dilations and the Loewner order

theorem HCPolySupport.HighContrast.smul_le_smul_of_le {n : Type u_1} {A B : Matrix n n ℝ} {c : ℝ} (hc : 0 ≤ c) (h : A ≤ B) : c • A ≤ c • B

Dilation by a nonnegative scalar is monotone for the Loewner order.

theorem HCPolySupport.HighContrast.posDef_conj {n : Type u_1} [Fintype n] [DecidableEq n] {Q C : Matrix n n ℝ} (hQ : Q.PosDef) (hC : IsUnit C) : (C.conjTranspose * Q * C).PosDef

Congruence by an invertible matrix preserves positive definiteness.

Normalization by the inverse square root

theorem HCPolySupport.HighContrast.conjTranspose_matSqrt_inv {n : Type u_1} [Fintype n] [DecidableEq n] {Q : Matrix n n ℝ} (hQ : Q.PosDef) : (matSqrt Q⁻¹).conjTranspose = matSqrt Q⁻¹

The inverse square root of a positive definite Q is symmetric.

theorem HCPolySupport.HighContrast.isUnit_matSqrt_inv {n : Type u_1} [Fintype n] [DecidableEq n] {Q : Matrix n n ℝ} (hQ : Q.PosDef) : IsUnit (matSqrt Q⁻¹)

The inverse square root of a positive definite matrix is invertible.

theorem HCPolySupport.HighContrast.conj_normalize {n : Type u_1} [Fintype n] [DecidableEq n] {P Q : Matrix n n ℝ} (hQ : Q.PosDef) (t : ℝ) : P ≤ t • Q ↔ matSqrt Q⁻¹ * P * matSqrt Q⁻¹ ≤ t • 1

Normalization. Conjugating by Q^{-1/2} turns a scalar Loewner bound against Q into a scalar Loewner bound against the identity, because the conjugation sends Q to 1.

theorem HCPolySupport.HighContrast.posSemidef_normalize {n : Type u_1} [Fintype n] [DecidableEq n] {P Q : Matrix n n ℝ} (hP : P.PosSemidef) (hQ : Q.PosDef) : (matSqrt Q⁻¹ * P * matSqrt Q⁻¹).PosSemidef

Normalization preserves positive semidefiniteness.

theorem HCPolySupport.HighContrast.posDef_normalize {n : Type u_1} [Fintype n] [DecidableEq n] {P Q : Matrix n n ℝ} (hP : P.PosDef) (hQ : Q.PosDef) : (matSqrt Q⁻¹ * P * matSqrt Q⁻¹).PosDef

Normalization preserves positive definiteness.

The relative size

noncomputable def HCPolySupport.HighContrast.relSize {n : Type u_1} [Fintype n] [DecidableEq n] (P Q : Matrix n n ℝ) : ℝ

The relative size Λ(Q;P) = |Q^{-1/2} P Q^{-1/2}| of P against Q: the scalar size of P measured in the geometry of Q.

Equations

• HCPolySupport.HighContrast.relSize P Q = ‖HCPolySupport.HighContrast.matSqrt Q⁻¹ * P * HCPolySupport.HighContrast.matSqrt Q⁻¹‖

theorem HCPolySupport.HighContrast.relSize_def {n : Type u_1} [Fintype n] [DecidableEq n] (P Q : Matrix n n ℝ) : relSize P Q = ‖matSqrt Q⁻¹ * P * matSqrt Q⁻¹‖

theorem HCPolySupport.HighContrast.relSize_nonneg {n : Type u_1} [Fintype n] [DecidableEq n] (P Q : Matrix n n ℝ) : 0 ≤ relSize P Q

theorem HCPolySupport.HighContrast.relSize_le_iff {n : Type u_1} [Fintype n] [DecidableEq n] {P Q : Matrix n n ℝ} (hP : P.PosSemidef) (hQ : Q.PosDef) {t : ℝ} (ht : 0 ≤ t) : relSize P Q ≤ t ↔ P ≤ t • Q

The relative size is the least scalar Loewner bound. This is the only property of relSize used downstream; everything below is a consequence.

theorem HCPolySupport.HighContrast.le_relSize_smul {n : Type u_1} [Fintype n] [DecidableEq n] {P Q : Matrix n n ℝ} (hP : P.PosSemidef) (hQ : Q.PosDef) : P ≤ relSize P Q • Q

The relative size realizes its own bound.

theorem HCPolySupport.HighContrast.relSize_self {n : Type u_1} [Fintype n] [DecidableEq n] {Q : Matrix n n ℝ} (hQ : Q.PosDef) : relSize Q Q = ‖1‖

The relative size of a positive definite matrix against itself is ‖1‖.

theorem HCPolySupport.HighContrast.relSize_self_eq_one {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] {Q : Matrix n n ℝ} (hQ : Q.PosDef) : relSize Q Q = 1

On a nonempty index type the relative size of a positive definite matrix against itself is one.

theorem HCPolySupport.HighContrast.relSize_mono_left {n : Type u_1} [Fintype n] [DecidableEq n] {P₁ P₂ Q : Matrix n n ℝ} (hP₁ : P₁.PosSemidef) (hP₂ : P₂.PosSemidef) (hQ : Q.PosDef) (h : P₁ ≤ P₂) : relSize P₁ Q ≤ relSize P₂ Q

The relative size is monotone in the numerator.

theorem HCPolySupport.HighContrast.relSize_anti_right {n : Type u_1} [Fintype n] [DecidableEq n] {P Q₁ Q₂ : Matrix n n ℝ} (hP : P.PosSemidef) (hQ₁ : Q₁.PosDef) (hQ₂ : Q₂.PosDef) (h : Q₁ ≤ Q₂) : relSize P Q₂ ≤ relSize P Q₁

The relative size is antitone in the denominator.

theorem HCPolySupport.HighContrast.relSize_smul_left {n : Type u_1} [Fintype n] [DecidableEq n] {c : ℝ} (hc : 0 ≤ c) (P Q : Matrix n n ℝ) : relSize (c • P) Q = c * relSize P Q

The relative size is homogeneous of degree one in the numerator.

theorem HCPolySupport.HighContrast.relSize_smul_right {n : Type u_1} [Fintype n] [DecidableEq n] {c : ℝ} (hc : 0 < c) {P Q : Matrix n n ℝ} (hP : P.PosSemidef) (hQ : Q.PosDef) : relSize P (c • Q) = c⁻¹ * relSize P Q

The relative size is homogeneous of degree minus one in the denominator.

theorem HCPolySupport.HighContrast.relSize_congr {n : Type u_1} [Fintype n] [DecidableEq n] {P Q C : Matrix n n ℝ} (hP : P.PosSemidef) (hQ : Q.PosDef) (hC : IsUnit C) : relSize (C.conjTranspose * P * C) (C.conjTranspose * Q * C) = relSize P Q

Invariance under a common congruence. Generalized eigenvalues do not see an invertible change of coordinates; this is the step the canonical balance takes when it moves the imbalance between E and its normalized form.

theorem HCPolySupport.HighContrast.relSize_one_left {n : Type u_1} [Fintype n] [DecidableEq n] {X : Matrix n n ℝ} (hX : X.PosDef) : relSize 1 X = ‖X⁻¹‖

Measuring the identity against a positive definite X reads off the size of X⁻¹.

theorem HCPolySupport.HighContrast.relSize_eq_norm_normalize_inv {n : Type u_1} [Fintype n] [DecidableEq n] {m₀ m₁ : Matrix n n ℝ} (h₀ : m₀.PosDef) (h₁ : m₁.PosDef) : relSize m₀ m₁ = ‖(matSqrt m₀⁻¹ * m₁ * matSqrt m₀⁻¹)⁻¹‖

The reciprocal reading of the relative size. With X := m₀^{-1/2} m₁ m₀^{-1/2}, the relative size of m₀ against m₁ is the size of X⁻¹, while the relative size of m₁ against m₀ is the size of X by definition. Since X is positive definite, ‖X‖ is its largest eigenvalue and ‖X⁻¹‖ the reciprocal of its smallest.

Two-sided comparison

theorem HCPolySupport.HighContrast.one_le_relSize_mul_relSize {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] {P Q : Matrix n n ℝ} (hP : P.PosDef) (hQ : Q.PosDef) : 1 ≤ relSize P Q * relSize Q P

The two relative sizes of a pair multiply to at least one. The product is the ratio of the largest to the smallest generalized eigenvalue.

theorem HCPolySupport.HighContrast.relSize_pos {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] {P Q : Matrix n n ℝ} (hP : P.PosDef) (hQ : Q.PosDef) : 0 < relSize P Q

The relative size of a pair of positive definite matrices is positive.