High-contrast homogenization: Geometry.AspectRatioOrder

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

The reference aspect ratio under the Schur ordering

The reference aspect ratio Π = Λ_0 / λ_0 of e.reference.aspect.ratio is not bounded below by one for an arbitrary symmetric positive definite doubled block: the doubled dilation c · I has Π = c², which is smaller than one for c < 1. What forces 1 ≤ Π is the ordering of the two symmetric Schur blocks of the parametrization e.annealed.schur, namely σ_* ≤ σ.

The proof is a chain of three Loewner inequalities. Positivity of the lower-right block makes the skew correction (k - h)ᵗ σ_*⁻¹ (k - h) nonnegative at every h, so σ ≤ σ + (k - h)ᵗ σ_*⁻¹ (k - h); evaluating at a skew matrix realizing Λ_0 gives σ ≤ Λ_0 · I. Conjugating by the square root of the lower-right block turns the definition of the spectral bound |σ_*⁻¹| into I ≤ |σ_*⁻¹| · σ_*. Composing the two through the hypothesis σ_* ≤ σ gives I ≤ (|σ_*⁻¹| Λ_0) · I, and testing against a vector of unit length reads off 1 ≤ Λ_0 |σ_*⁻¹| = Π.

The bound is sharp: at σ_* = σ the chain is an equality and Π = 1.

Quadratic-form bookkeeping

theorem HCPolySupport.HighContrast.matLoewnerLE_smul {d : ℕ} {c : ℝ} (hc : 0 ≤ c) {A B : Mat d} (h : MatLoewnerLE A B) : MatLoewnerLE (c • A) (c • B)

The Loewner order is preserved by nonnegative scaling.

The aspect ratio as a product

theorem HCPolySupport.HighContrast.aspectRatio_eq_bigLambdaRef_mul_specBound {d : ℕ} (E : BlockMat d) : aspectRatio E = bigLambdaRef E * specBound E.lowerRight

The aspect ratio Π = Λ_0 / λ_0 written as the product Λ_0 |σ_{*,0}^{-1}| of the two constants of e.reference.aspect.ratio.

The two halves of the chain

theorem HCPolySupport.HighContrast.matLoewnerLE_schurSigma_skewCorrectedForm {d : ℕ} {E : BlockMat d} (hpos : Book.Ch02.BlockPosDef E) (h : Mat d) : MatLoewnerLE (schurSigma E) (skewCorrectedForm E h)

The skew correction only increases the Schur block: σ ≤ σ + (k - h)ᵗ σ_*⁻¹ (k - h) at every h, because the lower-right block is positive.

theorem HCPolySupport.HighContrast.matLoewnerLE_schurSigma_bigLambdaRef_smul_one {d : ℕ} {E : BlockMat d} (hpos : Book.Ch02.BlockPosDef E) : MatLoewnerLE (schurSigma E) (bigLambdaRef E • 1)

The upper half of the chain: the Schur block σ is dominated by Λ_0 · I. The reference constant is realized at some skew matrix, and the skew-corrected form there dominates σ.

theorem HCPolySupport.HighContrast.matLoewnerLE_one_specBound_smul_schurSigmaStar {d : ℕ} {E : BlockMat d} (hsymm : IsSymmetricBlockMat E) (hpos : Book.Ch02.BlockPosDef E) : MatLoewnerLE 1 (specBound E.lowerRight • schurSigmaStar E)

The lower half of the chain: I ≤ |σ_{*,0}^{-1}| · σ_{*,0}. This is the definition of the spectral bound of the lower-right block, conjugated by the square root of that block, which carries σ_{*,0} to the identity.

The conclusion

theorem HCPolySupport.HighContrast.one_le_aspectRatio_of_schurSigmaStar_le {d : ℕ} [NeZero d] {E : BlockMat d} (hsymm : IsSymmetricBlockMat E) (hpos : Book.Ch02.BlockPosDef E) (horder : MatLoewnerLE (schurSigmaStar E) (schurSigma E)) : 1 ≤ aspectRatio E

The aspect ratio is at least one under the Schur ordering. For a symmetric positive definite doubled block whose two symmetric Schur blocks are ordered, σ_* ≤ σ, the reference aspect ratio Π of e.reference.aspect.ratio satisfies 1 ≤ Π.

The hypothesis cannot be dropped: the doubled dilation by c has σ = c · I, σ_* = c⁻¹ · I and Π = c², so Π < 1 exactly when the ordering fails. It is also not vacuous nor too strong: at c = 1 the ordering holds with equality and Π = 1, so the bound is attained.