High-contrast homogenization: Geometry.SizeAlignment

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

One scalar size, two encodings

A doubled block is measured against a positive reference block in two ways in this development.

The setup layer uses the Loewner recipe stated for the reference imbalance: blockSize H F is the least t ≥ 0 with -tF ≤ H ≤ tF, an infimum taken in the structural block dialect and involving no matrix square root. The canonical block geometry uses the spectral recipe relSize P Q = ‖Q^{-1/2} P Q^{-1/2}‖ on the flattened carrier.

On a positive semidefinite numerator and a positive definite denominator the two recipes name the same real number, and this file proves it. Two observations are all that is needed. First, relSize P Q is the least element of the set of nonnegative scalars t with P ≤ tQ, by relSize_le_iff together with le_relSize_smul, so it is that set's infimum. Second, the extra lower constraint -tF ≤ H carried by the defining set of blockSize is vacuous once 0 ≤ H, 0 ≤ F and 0 ≤ t, so the two defining sets coincide after the bridge of HCPoly.Geometry.BlockBridge transports the quadratic-form order to the Loewner order.

The consequence recorded last is the identity a consumer of the reference imbalance needs: the reference ratio κ_𝐄 of the setup layer and the imbalance 𝔡(𝐄) of e.response.canonical.imbalance are literally the same real number. The companion statement for the excess size reads blockExcess H F off the same relative size, normalized by one.

The relative size as an infimum

theorem HCPolySupport.HighContrast.isLeast_relSize {n : Type u_1} [Fintype n] [DecidableEq n] {P Q : Matrix n n ℝ} (hP : P.PosSemidef) (hQ : Q.PosDef) : IsLeast {t : ℝ | 0 ≤ t ∧ P ≤ t • Q} (relSize P Q)

The relative size is the least nonnegative scalar Loewner bound. This repackages relSize_le_iff and le_relSize_smul as an IsLeast statement.

Symmetry bookkeeping in the structural dialect

theorem HCPolySupport.HighContrast.isSymmetricBlockMat_blockScale {d : ℕ} (c : ℝ) {A : BlockMat d} (hA : IsSymmetricBlockMat A) : IsSymmetricBlockMat (blockScale c A)

A scalar dilation of a symmetric block is symmetric.

theorem HCPolySupport.HighContrast.isSymmetricBlockMat_of_isSymm_toFullBlockMat {d : ℕ} {A : BlockMat d} (hA : Matrix.IsSymm (toFullBlockMat A)) : IsSymmetricBlockMat A

Symmetry of the flattened matrix is structural symmetry; the converse of isSymm_toFullBlockMat.

theorem HCPolySupport.HighContrast.isSymmetricBlockMat_of_posSemidef {d : ℕ} {A : BlockMat d} (hA : Matrix.PosSemidef (toFullBlockMat A)) : IsSymmetricBlockMat A

A block whose flattening is positive semidefinite is symmetric.

The two scalar sizes agree

theorem HCPolySupport.HighContrast.blockSize_eq_relSize {d : ℕ} {H F : BlockMat d} (hH : IsSymmetricBlockMat H) (hF : IsSymmetricBlockMat F) (hFpd : Book.Ch02.BlockPosDef F) (hHps : Matrix.PosSemidef (toFullBlockMat H)) : blockSize H F = relSize (toFullBlockMat H) (toFullBlockMat F)

The setup layer's scalar size is the relative size of the canonical block geometry. Positive semidefiniteness of the numerator is what makes the lower Loewner constraint -tF ≤ H of blockSize vacuous, so that the defining set of blockSize H F is exactly the set of nonnegative scalar Loewner bounds whose least element is relSize.

theorem HCPolySupport.HighContrast.kappaRef_eq_canonImbalance {d : ℕ} {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) : kappaRef E = canonImbalance (toFullBlockMat E)

The reference ratio and the canonical imbalance are the same number. The setup layer's reference ratio κ_𝐄 = |𝐄_*^{-1/2}𝐄𝐄_*^{-1/2}| and the imbalance 𝔡(𝐄) of e.response.canonical.imbalance agree on every positive symmetric block.

theorem HCPolySupport.HighContrast.blockExcess_eq {d : ℕ} {H F : BlockMat d} (hH : IsSymmetricBlockMat H) (hF : IsSymmetricBlockMat F) (hFpd : Book.Ch02.BlockPosDef F) (hHps : Matrix.PosSemidef (toFullBlockMat H)) : blockExcess H F = max (relSize (toFullBlockMat H) (toFullBlockMat F) - 1) 0

The excess size is the relative size, normalized by one. The set defining blockExcess H F is the set of t ≥ 0 with relSize ≤ 1 + t, so it is a closed half-line and its infimum is the positive part of relSize - 1.