High-contrast homogenization: Geometry.SqrtOrder

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

Operator monotonicity of the square root

The joint monotonicity of the matrix geometric mean rests on the fact that H ↦ H^{1/2} is monotone for the Loewner order. The reference text proves that from the integral representation of the matrix square root; the argument here is the equivalent norm argument, which needs no vector-valued integral.

Write S, T for the square roots of A ≤ B, with B positive definite, and put W := T^{-1/2} S T^{-1/2}. Conjugating A ≤ B by T^{-1} shows that (S T^{-1})^t (S T^{-1}) ≤ I, so ‖S T^{-1}‖ ≤ 1. The powers of W telescope through S T^{-1}, so ‖W^m‖ is bounded uniformly in m, while ‖W^{2^k}‖ equals ‖W‖^{2^k} because W is symmetric. Hence ‖W‖ ≤ 1, that is W ≤ I, and conjugating back gives S ≤ T.

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

Operator monotonicity of the square root. This is the substantive step in the joint monotonicity of the matrix geometric mean.