High-contrast homogenization: Entry.Analysis.ContrastOrder

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

Monotonicity of the intrinsic contrast in the Loewner order

The intrinsic contrast of e.Theta.m is the infimum over skew h of the scalings t with σ + (k - h)ᵗ σ_*⁻¹ (k - h) ≤ t σ_*. Both sides of this comparison are monotone in the doubled block matrix: the quadratic form of the left side at e is the doubled quadratic form at the block vector (e, h e), and σ_* is the inverse of the lower-right block, which is antitone in the Loewner order. Hence a Loewner comparison A ≤ B of two symmetric positive definite doubled block matrices forces Θ(A) ≤ Θ(B), with the minimizing skew matrix of B admissible for A.

Vector algebra

Block symmetry

The skew-corrected form as a doubled quadratic form

Order consequences of a Loewner comparison

theorem HCPolySupport.HighContrast.blockPosDef_of_blockMatLoewnerLE {d : ℕ} {A B : BlockMat d} (hApos : Book.Ch02.BlockPosDef A) (hAB : BlockMatLoewnerLE A B) : Book.Ch02.BlockPosDef B

Positivity passes up the doubled Loewner order.

theorem HCPolySupport.HighContrast.matLoewnerLE_inv_of_matLoewnerLE {d : ℕ} {L M : Mat d} (hL : Matrix.PosDef L) (hM : Matrix.PosDef M) (hLM : MatLoewnerLE L M) : MatLoewnerLE M⁻¹ L⁻¹

Antitonicity of the inverse. On positive definite matrices the Loewner order is reversed by inversion.

theorem HCPolySupport.HighContrast.matLoewnerLE_schurSigmaStar_of_blockMatLoewnerLE {d : ℕ} {A B : BlockMat d} (hAsymm : IsSymmetricBlockMat A) (hApos : Book.Ch02.BlockPosDef A) (hBsymm : IsSymmetricBlockMat B) (hAB : BlockMatLoewnerLE A B) : MatLoewnerLE (schurSigmaStar B) (schurSigmaStar A)

The Schur block σ_* is antitone in the doubled Loewner order: A ≤ B gives σ_*(B) ≤ σ_*(A).

theorem HCPolySupport.HighContrast.exists_isSkewMat_matLoewnerLE_blockContrast_smul {d : ℕ} {H : BlockMat d} (hsymm : IsSymmetricBlockMat H) (hpos : Book.Ch02.BlockPosDef H) : ∃ (h : Mat d), IsSkewMat h ∧ MatLoewnerLE (skewCorrectedForm H h) (blockContrast H • schurSigmaStar H)

The intrinsic contrast of a symmetric positive definite doubled block matrix is itself an admissible Loewner scaling: some skew h realizes it.

Monotonicity of the intrinsic contrast

theorem HCPolySupport.HighContrast.blockContrast_le_of_blockMatLoewnerLE {d : ℕ} {A B : BlockMat d} (hAsymm : IsSymmetricBlockMat A) (hApos : Book.Ch02.BlockPosDef A) (hBsymm : IsSymmetricBlockMat B) (hAB : BlockMatLoewnerLE A B) : blockContrast A ≤ blockContrast B

Monotonicity of the intrinsic contrast. If A ≤ B in the doubled Loewner order, with A symmetric positive definite and B symmetric, then Θ(A) ≤ Θ(B): the skew matrix realizing Θ(B) is admissible for A at the same scaling, because the skew-corrected form of A at (e, h e) lies below that of B, while σ_*(B) ≤ σ_*(A).