High-contrast homogenization: Geometry.OperatorOrder

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

The Loewner order, the spectral norm, and the square root

The canonical block geometry built on the matrix geometric mean is read entirely through the Loewner order on real symmetric matrices, written ≤ here, and the spectral norm |·|, written ‖·‖. This file collects the interface between the two:

• congruence A ≤ B → Cᵀ A C ≤ Cᵀ B C, and its converse for invertible C;
• the scalar comparison ‖A‖ ≤ t ↔ A ≤ t • I on positive semidefinite data, which is the statement that ‖A‖ is the largest eigenvalue;
• order reversal under inversion;
• operator monotonicity of the square root.

Only the last one is not immediate. The reference text proves it from the integral representation of the square root; the proof given here is the equivalent norm argument: writing S, T for the roots of A ≤ B and W := T^{-1/2} S T^{-1/2}, the powers W^m factor through S T^{-1}, whose norm the hypothesis bounds by one, so ‖W‖^m stays bounded and ‖W‖ ≤ 1.

The scalar sizes of the reference text are spectral norms of positive semidefinite matrices throughout this development. The setup layer's specBound is the same number (specBound_eq_norm); ‖·‖ is used here because the geometry is built on index types other than Fin d.

Real transposes

theorem HCPolySupport.HighContrast.conjTranspose_eq_transpose' {n : Type u_1} (A : Matrix n n ℝ) : A.conjTranspose = A.transpose

Over the reals the conjugate transpose is the transpose.

theorem HCPolySupport.HighContrast.isHermitian_of_isSymm {n : Type u_1} {A : Matrix n n ℝ} (h : A.IsSymm) : A.IsHermitian

A symmetric real matrix is Hermitian.

theorem HCPolySupport.HighContrast.isSymm_of_isHermitian {n : Type u_1} {A : Matrix n n ℝ} (h : A.IsHermitian) : A.IsSymm

A Hermitian real matrix is symmetric.

Congruence

theorem HCPolySupport.HighContrast.conj_le_conj {n : Type u_1} [Fintype n] {A B : Matrix n n ℝ} (C : Matrix n n ℝ) (h : A ≤ B) : C.conjTranspose * A * C ≤ C.conjTranspose * B * C

Congruence is monotone. Conjugating both sides of a Loewner inequality by the same matrix preserves it.

theorem HCPolySupport.HighContrast.conj_le_conj_iff {n : Type u_1} [Fintype n] [DecidableEq n] {A B C : Matrix n n ℝ} (hC : IsUnit C) : C.conjTranspose * A * C ≤ C.conjTranspose * B * C ↔ A ≤ B

Congruence by an invertible matrix reflects the order.

theorem HCPolySupport.HighContrast.conj_le_conj' {n : Type u_1} [Fintype n] {A B C : Matrix n n ℝ} (hC : C.conjTranspose = C) (h : A ≤ B) : C * A * C ≤ C * B * C

Congruence by a symmetric matrix, in the form the block geometry uses.

The scalar comparison

theorem HCPolySupport.HighContrast.dotProduct_mulVec_symm {n : Type u_1} [Fintype n] {A : Matrix n n ℝ} (hA : A.transpose = A) (x y : n → ℝ) : x ⬝ᵥ A.mulVec y = A.mulVec x ⬝ᵥ y

A symmetric matrix moves across the Euclidean pairing.

theorem HCPolySupport.HighContrast.dotProduct_mulVec_le_norm_mul {n : Type u_1} [Fintype n] [DecidableEq n] (A : Matrix n n ℝ) (x : n → ℝ) : x ⬝ᵥ A.mulVec x ≤ ‖A‖ * x ⬝ᵥ x

The quadratic form is controlled by the spectral norm, for every matrix.

theorem HCPolySupport.HighContrast.norm_le_of_le_smul_one {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.PosSemidef) {t : ℝ} (ht : 0 ≤ t) (h : A ≤ t • 1) : ‖A‖ ≤ t

A matrix bounded by t • I in the Loewner order has spectral norm at most t, on positive semidefinite data.

theorem HCPolySupport.HighContrast.le_smul_one_of_norm_le {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.PosSemidef) {t : ℝ} (h : ‖A‖ ≤ t) : A ≤ t • 1

A matrix of spectral norm at most t is bounded by t • I in the Loewner order, on positive semidefinite data.

theorem HCPolySupport.HighContrast.norm_le_iff_le_smul_one {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.PosSemidef) {t : ℝ} (ht : 0 ≤ t) : ‖A‖ ≤ t ↔ A ≤ t • 1

The spectral norm is the least scalar Loewner bound. On positive semidefinite data ‖A‖ is the reference text's |A|.

theorem HCPolySupport.HighContrast.le_norm_smul_one {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.PosSemidef) : A ≤ ‖A‖ • 1

A positive semidefinite matrix is bounded by its own spectral norm.

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

The spectral norm is monotone for the Loewner order on positive semidefinite data.

theorem HCPolySupport.HighContrast.posDef_of_posDef_le {n : Type u_1} [Finite n] {A B : Matrix n n ℝ} (hA : A.PosDef) (hAB : A ≤ B) : B.PosDef

A matrix dominating a positive definite matrix is positive definite.

The square root as a unit

theorem HCPolySupport.HighContrast.matSqrt_eq_cfcSqrt {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.PosSemidef) : matSqrt A = CFC.sqrt A

matSqrt agrees with the C⋆ functional-calculus square root on positive semidefinite data, so the two APIs may be mixed freely.

theorem HCPolySupport.HighContrast.isUnit_det_of_posDef {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.PosDef) : IsUnit A.det

The determinant of a positive definite matrix is a unit.

theorem HCPolySupport.HighContrast.posDef_of_posSemidef_of_isUnit {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.PosSemidef) (hu : IsUnit A) : A.PosDef

A positive semidefinite unit is positive definite.

theorem HCPolySupport.HighContrast.isUnit_matSqrt {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.PosDef) : IsUnit (matSqrt A)

The square root of a positive definite matrix is a unit.

theorem HCPolySupport.HighContrast.posDef_matSqrt {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.PosDef) : (matSqrt A).PosDef

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

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

The square root of the inverse is the inverse of the square root.

theorem HCPolySupport.HighContrast.transpose_matSqrt_inv {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.PosDef) : (matSqrt A⁻¹).transpose = matSqrt A⁻¹

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

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

The inverse square root normalizes. Conjugating a positive definite matrix by its own inverse square root gives the identity; this is the substitution the reference text writes as A^{-1/2} A A^{-1/2} = I.

Order reversal under inversion

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

Inversion reverses the Loewner order.