Coarse-graining support: Support.Ambient.MatrixOrderBridge #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Ambient matrix-order bridges #
Conversion lemmas between the local quadratic-form order MatLoewnerLE used in
the homogenization development and mathlib's matrix order, together with the
basic inverse-antitonicity consequence for positive-definite real matrices.
theorem
HCPolySupport.matLoewnerLE_matrixOrder_of_posSemidef
{d : ℕ}
{A B : Mat d}
(hA : Matrix.PosSemidef A)
(hB : Matrix.PosSemidef B)
(hAB : MatLoewnerLE A B)
:
theorem
HCPolySupport.matLoewnerLE_of_matrixOrder_of_posSemidef
{d : ℕ}
{A B : Mat d}
(_hA : Matrix.PosSemidef A)
(_hB : Matrix.PosSemidef B)
(hAB : A ≤ B)
:
MatLoewnerLE A B
theorem
HCPolySupport.matLoewnerLE_inv_of_posDef
{d : ℕ}
{A B : Mat d}
(hA : Matrix.PosDef A)
(hB : Matrix.PosDef B)
(hAB : MatLoewnerLE A B)
:
MatLoewnerLE B⁻¹ A⁻¹