High-contrast homogenization: Geometry.GeometricMeanToolkit

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

The geometric-mean toolkit

The algebraic rules for the matrix geometric mean: it is symmetric, commutes with inversion, is equivariant under congruence, is jointly monotone for the Loewner order, is homogeneous of degree one half in each argument, and has determinant the geometric mean of the two determinants.

Except for monotonicity, each clause is obtained by exhibiting the candidate as a positive solution of the Riccati equation of the target pair and appealing to eq_matGeomMean_of_riccati. Monotonicity is read off the defining formula, and is where operator monotonicity of the square root enters.

Idempotence, symmetry, inversion

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

The geometric mean of a matrix with itself is that matrix.

theorem HCPolySupport.HighContrast.inv_riccati {n : Type u_1} [Fintype n] [DecidableEq n] {A B X : Matrix n n ℝ} (h : X * A⁻¹ * X = B) : X⁻¹ * A⁻¹⁻¹ * X⁻¹ = B⁻¹

Inverting the Riccati equation of the pair (A, B) gives the Riccati equation of the pair (A⁻¹, B⁻¹) for the inverse mean.

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

The inverse formula (A # B)⁻¹ = A⁻¹ # B⁻¹.

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

Symmetry A # B = B # A.

Congruence

theorem HCPolySupport.HighContrast.matGeomMean_conj {n : Type u_1} [Fintype n] [DecidableEq n] {A B C : Matrix n n ℝ} (hA : A.PosDef) (hB : B.PosDef) (hC : IsUnit C) : matGeomMean (C.conjTranspose * A * C) (C.conjTranspose * B * C) = C.conjTranspose * matGeomMean A B * C

Congruence equivariance (Cᵗ A C) # (Cᵗ B C) = Cᵗ (A # B) C.

Monotonicity

theorem HCPolySupport.HighContrast.matGeomMean_mono_right {n : Type u_1} [Fintype n] [DecidableEq n] {A B₀ B₁ : Matrix n n ℝ} (hA : A.PosDef) (hB₀ : B₀.PosDef) (hB₁ : B₁.PosDef) (h : B₀ ≤ B₁) : matGeomMean A B₀ ≤ matGeomMean A B₁

The geometric mean is monotone in its second argument.

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

Joint monotonicity of the geometric mean.

Homogeneity and the determinant

theorem HCPolySupport.HighContrast.posDef_smul {n : Type u_1} {A : Matrix n n ℝ} (hA : A.PosDef) {c : ℝ} (hc : 0 < c) : (c • A).PosDef

The dilation of a positive definite matrix by a positive scalar is positive definite.

theorem HCPolySupport.HighContrast.matGeomMean_smul {n : Type u_1} [Fintype n] [DecidableEq n] {A B : Matrix n n ℝ} (hA : A.PosDef) (hB : B.PosDef) {a b : ℝ} (ha : 0 < a) (hb : 0 < b) : matGeomMean (a • A) (b • B) = √(a * b) • matGeomMean A B

Homogeneity (a A) # (b B) = (a b)^{1/2} (A # B).

theorem HCPolySupport.HighContrast.det_matGeomMean {n : Type u_1} [Fintype n] [DecidableEq n] {A B : Matrix n n ℝ} (hA : A.PosDef) (hB : B.PosDef) : (matGeomMean A B).det = √(A.det * B.det)

The determinant of the geometric mean is the geometric mean of the determinants.