High-contrast homogenization: Geometry.AspectRatioMonotone

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

Monotonicity of the reference aspect ratio

The aspect ratio Π of e.reference.aspect.ratio is monotone for the quadratic form order on symmetric positive definite doubled blocks: if A ≤ E then Π(A) ≤ Π(E).

Both factors of Π = Λ_0 |σ_{*,0}^{-1}| are monotone, for different reasons. The spectral bound of the lower-right block is monotone because the doubled order restricts to the lower-right corner along the vectors (0, q).

The constant Λ_0 is monotone because of a slice identity: at a fixed h, the skew-corrected form of e.reference.aspect.ratio is the doubled quadratic form evaluated on the graph of h,

p · (σ + (k - h)ᵗ σ_*⁻¹ (k - h)) p = (p, h p) · H (p, h p),

which is checked by expanding the Schur parametrization into σ + (k - h)ᵗ σ_*⁻¹ (k - h) = H₁₁ + H₁₂ h + hᵗ H₂₁ + hᵗ H₂₂ h. So a doubled inequality between blocks gives, at every fixed h, an inequality of skew-corrected forms, and the defining infima are then compared term by term.

The slice identity

theorem HCPolySupport.HighContrast.skewCorrectedForm_eq_of_isSymmetricBlockMat {d : ℕ} {H : BlockMat d} (hsymm : IsSymmetricBlockMat H) (hdet : IsUnit (Matrix.det H.lowerRight)) (h : Mat d) : skewCorrectedForm H h = H.upperLeft + H.upperRight * h + matTranspose h * H.lowerLeft + matTranspose h * H.lowerRight * h

The skew-corrected form of e.reference.aspect.ratio expanded in the four corners: σ + (k - h)ᵗ σ_*⁻¹ (k - h) = H₁₁ + H₁₂ h + hᵗ H₂₁ + hᵗ H₂₂ h. The Schur relations H₂₂ k = -H₂₁ and kᵗ H₂₂ = -H₁₂ cancel every term carrying the Schur skew block k.

theorem HCPolySupport.HighContrast.vecDot_matVecMul_skewCorrectedForm {d : ℕ} {H : BlockMat d} (hsymm : IsSymmetricBlockMat H) (hdet : IsUnit (Matrix.det H.lowerRight)) (h : Mat d) (p : Vec d) : vecDot p (matVecMul (skewCorrectedForm H h) p) = blockVecDot (p, matVecMul h p) (blockMatVecMul H (p, matVecMul h p))

The slice identity. The quadratic form of the skew-corrected form at p is the doubled quadratic form of the block at the vector (p, h p).

Monotonicity of the two factors

theorem HCPolySupport.HighContrast.matLoewnerLE_lowerRight_of_blockMatLoewnerLE {d : ℕ} {A E : BlockMat d} (hle : BlockMatLoewnerLE A E) : MatLoewnerLE A.lowerRight E.lowerRight

The doubled order restricts to the lower-right corner.

theorem HCPolySupport.HighContrast.matLoewnerLE_skewCorrectedForm_of_blockMatLoewnerLE {d : ℕ} {A E : BlockMat d} (hAsymm : IsSymmetricBlockMat A) (hApos : Book.Ch02.BlockPosDef A) (hEsymm : IsSymmetricBlockMat E) (hEpos : Book.Ch02.BlockPosDef E) (hle : BlockMatLoewnerLE A E) (h : Mat d) : MatLoewnerLE (skewCorrectedForm A h) (skewCorrectedForm E h)

At a fixed skew parameter the skew-corrected form is monotone in the block, by the slice identity.

theorem HCPolySupport.HighContrast.bigLambdaRef_mono {d : ℕ} {A E : BlockMat d} (hAsymm : IsSymmetricBlockMat A) (hApos : Book.Ch02.BlockPosDef A) (hEsymm : IsSymmetricBlockMat E) (hEpos : Book.Ch02.BlockPosDef E) (hle : BlockMatLoewnerLE A E) : bigLambdaRef A ≤ bigLambdaRef E

The reference constant Λ_0 is monotone: the defining set of thresholds only grows as the block decreases.

The conclusion

theorem HCPolySupport.HighContrast.aspectRatio_mono {d : ℕ} {A E : BlockMat d} (hAsymm : IsSymmetricBlockMat A) (hApos : Book.Ch02.BlockPosDef A) (hEsymm : IsSymmetricBlockMat E) (hEpos : Book.Ch02.BlockPosDef E) (hle : BlockMatLoewnerLE A E) : aspectRatio A ≤ aspectRatio E

The aspect ratio is monotone for the quadratic form order on symmetric positive definite doubled blocks.