Documentation

LeanPool.HighContrastHomogenization.Geometry.GeometricMean

High-contrast homogenization: Geometry.GeometricMean #

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

The matrix geometric mean #

For positive matrices A and B of the same size the reference text sets A # B := A^{1/2}(A^{-1/2} B A^{-1/2})^{1/2} A^{1/2} and characterizes it as the unique positive solution X of the Riccati equation X A^{-1} X = B; the mean and its properties are the ones used in p.global.selection. This file carries out that characterization and the algebraic rules that follow from it: symmetry, the inverse formula, congruence, joint monotonicity, homogeneity, and the determinant.

The characterization is the substitution Y := A^{-1/2} X A^{-1/2}, under which X A^{-1} X = B becomes Y^2 = A^{-1/2} B A^{-1/2}; since a positive matrix has exactly one positive square root, the solution is unique and is the displayed formula. Every clause of the toolkit except monotonicity is then a one-line manipulation of the Riccati equation followed by uniqueness. Monotonicity uses operator monotonicity of the square root, which is matSqrt_le_matSqrt.

source
noncomputable def HCPolySupport.HighContrast.matGeomMean {n : Type u_1} [Fintype n] [DecidableEq n] (A B : Matrix n n ℝ) :
Matrix n n ℝ

The matrix geometric mean A # B = A^{1/2}(A^{-1/2} B A^{-1/2})^{1/2} A^{1/2} of the reference text.

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    Bookkeeping for the two square roots #

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

    The inverse square root cancels the square root.

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

    The square root cancels the inverse square root.

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

    The inverse square root squares to the inverse.

    source
    theorem HCPolySupport.HighContrast.conjTranspose_matSqrt {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.PosSemidef) :
    (matSqrt A).conjTranspose = matSqrt A

    The square root is symmetric.

    The Riccati characterization #

    source
    theorem HCPolySupport.HighContrast.posDef_matGeomMean {n : Type u_1} [Fintype n] [DecidableEq n] {A B : Matrix n n ℝ} (hA : A.PosDef) (hB : B.PosDef) :
    (matGeomMean A B).PosDef

    The geometric mean is positive definite.

    source
    theorem HCPolySupport.HighContrast.matGeomMean_riccati {n : Type u_1} [Fintype n] [DecidableEq n] {A B : Matrix n n ℝ} (hA : A.PosDef) (hB : B.PosDef) :
    matGeomMean A B * A⁻¹ * matGeomMean A B = B

    The Riccati equation: the geometric mean solves X A^{-1} X = B.

    source
    theorem HCPolySupport.HighContrast.eq_matGeomMean_of_riccati {n : Type u_1} [Fintype n] [DecidableEq n] {A B X : Matrix n n ℝ} (hA : A.PosDef) (hX : X.PosDef) (h : X * A⁻¹ * X = B) :
    X = matGeomMean A B

    Riccati uniqueness. A positive solution of X A^{-1} X = B is the geometric mean.

    source
    theorem HCPolySupport.HighContrast.existsUnique_riccati {n : Type u_1} [Fintype n] [DecidableEq n] {A B : Matrix n n ℝ} (hA : A.PosDef) (hB : B.PosDef) :
    ∃! X : Matrix n n ℝ, X.PosDef ∧ X * A⁻¹ * X = B

    The Riccati characterization, existence and uniqueness. The geometric mean is the unique positive solution of the Riccati equation.