High-contrast homogenization: Entry.Geometry.PositiveSqrtCongruence #

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

Positive Sqrt Congruence #

The positive square root 𝔪^{1/2} of a positive definite matrix 𝔪, and the congruence identity that compares relative matrices in the Loewner order. For a positive definite 𝔪 the module proves that CFC.sqrt 𝔪 is positive definite, that CFC.sqrt 𝔪 * CFC.sqrt 𝔪 = 𝔪, and the two eigenvalue bounds of the print: ⟨v, 𝔪^{1/2} v⟩ ≤ |𝔪|^{1/2} |v|² for the largest eigenvalue and |v|² ≤ |𝔪⁻¹|^{1/2} ⟨v, 𝔪^{1/2} v⟩ for the smallest. These are the matrix ingredients of e.rounded.grid.bounds. The module then proves that congruence A ↦ Pᵀ A P preserves the Loewner order and, for invertible P, reflects it as well, which is the substitution that compares relative matrices.

The positive square root `𝔪^{1/2}` #

The print's 𝔪^{1/2} for a positive matrix 𝔪 is Mathlib's CFC.sqrt 𝔪, the positive semidefinite square root from the continuous functional calculus (Mathlib.Analysis.Matrix.Order sets this up on real matrices under open scoped MatrixOrder).

What e.rounded.grid.bounds needs about it is the two eigenvalue statements of the print, "the unrounded matrix |𝔪⁻¹|^{1/2} 𝔪^{1/2} has smallest eigenvalue one and largest eigenvalue (|𝔪| |𝔪⁻¹|)^{1/2}", in the form of two-sided bounds on the quadratic form of 𝔪^{1/2}:

⟨v, 𝔪^{1/2} v⟩ ≤ |𝔪|^{1/2} |v|², and
|v|² ≤ |𝔪⁻¹|^{1/2} ⟨v, 𝔪^{1/2} v⟩.

Both are proved without the spectral theorem: the first from |𝔪^{1/2} v|² = ⟨v, 𝔪 v⟩, the second by the same argument applied to (𝔪^{1/2})⁻¹, whose square is 𝔪⁻¹, together with Cauchy–Schwarz for the positive form of (𝔪^{1/2})⁻¹.

source

theorem HCPolySupport.HighContrast.Geometry.posDef_sqrt {d : ℕ} {m : Mat d} (hm : Matrix.PosDef m) :

(CFC.sqrt m).PosDef

source

theorem HCPolySupport.HighContrast.Geometry.sqrt_mul_sqrt {d : ℕ} {m : Mat d} (hm : Matrix.PosDef m) :

CFC.sqrt m * CFC.sqrt m = m

source

theorem HCPolySupport.HighContrast.Geometry.transpose_sqrt {d : ℕ} {m : Mat d} (hm : Matrix.PosDef m) :

(CFC.sqrt m).transpose = CFC.sqrt m

source

theorem HCPolySupport.HighContrast.Geometry.sqrt_apply_comm {d : ℕ} {m : Mat d} (hm : Matrix.PosDef m) (a b : Fin d) :

CFC.sqrt m b a = CFC.sqrt m a b

source

theorem HCPolySupport.HighContrast.Geometry.dotProduct_sqrt_nonneg {d : ℕ} {m : Mat d} (hm : Matrix.PosDef m) (v : Vec d) :

0 ≤ v ⬝ᵥ (CFC.sqrt m).mulVec v

source

theorem HCPolySupport.HighContrast.Geometry.dotProduct_sqrt_le {d : ℕ} {m : Mat d} (hm : Matrix.PosDef m) (v : Vec d) :

v ⬝ᵥ (CFC.sqrt m).mulVec v ≤ √‖m‖ * vecNormSq v

The largest eigenvalue of 𝔪^{1/2} is at most |𝔪|^{1/2}: ⟨v, 𝔪^{1/2} v⟩ ≤ √‖𝔪‖ |v|².

source

theorem HCPolySupport.HighContrast.Geometry.vecNormSq_le_sqrt_opNorm_inv_mul_dotProduct_sqrt {d : ℕ} {m : Mat d} (hm : Matrix.PosDef m) (v : Vec d) :

vecNormSq v ≤ √‖m⁻¹ ‖ * v ⬝ᵥ (CFC.sqrt m).mulVec v

The smallest eigenvalue of 𝔪^{1/2} is at least |𝔪⁻¹|^{-1/2}: |v|² ≤ √‖𝔪⁻¹‖ ⟨v, 𝔪^{1/2} v⟩.

Congruence for the Loewner order #

This file proves the quadratic-form congruence layer needed to compare the relative matrix m₀^{-1/2} m₁ m₀^{-1/2} with the MatLoewnerLE thresholds. The congruence is purely by substitution in the quadratic form; no commutativity between the two endpoint matrices is used.

source