High-contrast homogenization: Setup.SpectralBound

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

The scalar Loewner bound and the positive semidefinite square root

The reference text writes |M| for the spectral norm of a symmetric positive semidefinite matrix and m^{1/2} for the positive square root. This file proves that the encodings specBound and matSqrt are those objects: specBound M is the least t ≥ 0 with M ≤ t I, and matSqrt M is the positive semidefinite square root, independently of the choice made in its definition.

theorem HCPolySupport.HighContrast.specBound_nonneg {d : ℕ} (M : Mat d) : 0 ≤ specBound M

specBound is nonnegative, junk branch included.

theorem HCPolySupport.HighContrast.specBound_le {d : ℕ} {M : Mat d} {t : ℝ} (h0 : 0 ≤ t) (h : MatLoewnerLE M (t • 1)) : specBound M ≤ t

specBound M is a lower bound for the admissible scalar Loewner bounds.

theorem HCPolySupport.HighContrast.matLoewnerLE_smul_one_of_le {d : ℕ} {s t : ℝ} (hst : s ≤ t) : MatLoewnerLE (s • 1) (t • 1)

The scalar Loewner order between multiples of the identity.

theorem HCPolySupport.HighContrast.exists_matLoewnerLE_smul_one {d : ℕ} (M : Mat d) : ∃ (t : ℝ), 0 ≤ t ∧ MatLoewnerLE M (t • 1)

Every matrix admits a scalar Loewner bound, so the infimum defining specBound is taken over a nonempty set.

theorem HCPolySupport.HighContrast.matLoewnerLE_specBound_smul_one {d : ℕ} (M : Mat d) : MatLoewnerLE M (specBound M • 1)

specBound M is itself an admissible scalar Loewner bound.

theorem HCPolySupport.HighContrast.specBound_le_iff {d : ℕ} {M : Mat d} {t : ℝ} (ht : 0 ≤ t) : specBound M ≤ t ↔ MatLoewnerLE M (t • 1)

specBound characterization. specBound M is the least nonnegative t with M ≤ t I; on symmetric positive semidefinite data this is the norm |M| of the reference text.

The positive semidefinite square root

theorem HCPolySupport.HighContrast.exists_posSemidef_mul_self {n : Type u_1} [Fintype n] {M : Matrix n n ℝ} (hM : M.PosSemidef) : ∃ (B : Matrix n n ℝ), B.PosSemidef ∧ B * B = M

The positive semidefinite square root exists on positive semidefinite data.

theorem HCPolySupport.HighContrast.posSemidef_mul_self_unique {n : Type u_1} [Fintype n] {M B B' : Matrix n n ℝ} (hB : B.PosSemidef) (hB' : B'.PosSemidef) (h : B * B = M) (h' : B' * B' = M) : B = B'

The positive semidefinite square root is unique.

theorem HCPolySupport.HighContrast.matSqrt_spec {n : Type u_1} [Fintype n] [DecidableEq n] {M : Matrix n n ℝ} (hM : M.PosSemidef) : (matSqrt M).PosSemidef ∧ matSqrt M * matSqrt M = M

Specification of matSqrt on positive semidefinite data.

theorem HCPolySupport.HighContrast.matSqrt_eq {n : Type u_1} [Fintype n] [DecidableEq n] {M B : Matrix n n ℝ} (hM : M.PosSemidef) (hB : B.PosSemidef) (h : B * B = M) : matSqrt M = B

matSqrt is independent of the choice made in its definition: it is the unique positive semidefinite square root.

Junk guards on the contrast constants

theorem HCPolySupport.HighContrast.blockContrast_nonneg {d : ℕ} (H : BlockMat d) : 0 ≤ blockContrast H

The intrinsic contrast is nonnegative, junk branch included.

theorem HCPolySupport.HighContrast.blockContrast_le {d : ℕ} {H : BlockMat d} {t : ℝ} (h0 : 0 ≤ t) {h : Mat d} (hskew : IsSkewMat h) (hle : MatLoewnerLE (schurSigma H + matTranspose (schurSkew H - h) * H.lowerRight * (schurSkew H - h)) (t • schurSigmaStar H)) : blockContrast H ≤ t

The intrinsic contrast is a lower bound for the admissible Loewner scalings.

theorem HCPolySupport.HighContrast.bigLambdaRef_nonneg {d : ℕ} (E : BlockMat d) : 0 ≤ bigLambdaRef E

Λ_0 is nonnegative, junk branch included.

theorem HCPolySupport.HighContrast.aspectRatio_nonneg {d : ℕ} (E : BlockMat d) : 0 ≤ aspectRatio E

The reference aspect ratio is nonnegative, so the logarithm of 2 + Π K in the entry theorem is taken at an argument at least 2.