High-contrast homogenization: Setup.Contrast

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

The intrinsic contrast in the printed form

The reference text writes the intrinsic contrast of a doubled block matrix as the minimum over skew h of the conjugated norms |σ_*^{-1/2}(σ + (k - h)ᵗ σ_*⁻¹ (k - h)) σ_*^{-1/2}| (the intrinsic contrast of the reference block, and e.Theta.m), and the reference constant Λ_0 as the corresponding unconjugated minimum (e.reference.aspect.ratio). This file proves that the Loewner-scaling encodings blockContrast and bigLambdaRef are the infima of exactly those families: the conjugation identity turns comparison with t σ_* into comparison of the conjugate with t I, and the threshold form of the infimum is the infimum of the family.

Infima over the skew parameter

theorem HCPolySupport.HighContrast.isSkewMat_zero {d : ℕ} : IsSkewMat 0

theorem HCPolySupport.HighContrast.sInf_skew_eq {d : ℕ} {f : Mat d → ℝ} (hf : ∀ (h : Mat d), 0 ≤ f h) : sInf {t : ℝ | 0 ≤ t ∧ ∃ (h : Mat d), IsSkewMat h ∧ f h ≤ t} = sInf (f '' {h : Mat d | IsSkewMat h})

The threshold form of an infimum over a nonnegative family indexed by the skew matrices is the infimum of the family.

noncomputable def HCPolySupport.HighContrast.skewCorrectedForm {d : ℕ} (H : BlockMat d) (h : Mat d) : Mat d

The skew-corrected Schur form σ + (k - h)ᵗ σ_*⁻¹ (k - h) of a doubled block matrix: the matrix whose norm the reference text minimizes over skew h.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.bigLambdaRef_eq_sInf {d : ℕ} (E : BlockMat d) : bigLambdaRef E = sInf ((fun (h : Mat d) => specBound (skewCorrectedForm E h)) '' {h : Mat d | IsSkewMat h})

Λ_0 in printed form. The reference constant is the infimum over skew h of the norms |σ_0 + (k_0 - h)ᵗ σ_{*,0}^{-1} (k_0 - h)|.

The conjugation identity

theorem HCPolySupport.HighContrast.matLoewnerLE_smul_iff_conj {d : ℕ} {σ R M : Mat d} (hR : matTranspose R = R) (hRR : R * σ * R = 1) (hRinv : IsUnit (Matrix.det R)) (t : ℝ) : MatLoewnerLE M (t • σ) ↔ MatLoewnerLE (R * M * R) (t • 1)

The conjugation identity. For an invertible symmetric R with R σ R = 1, comparison with t σ in the Loewner order is comparison of the conjugate R M R with t I.

Positivity of the Schur block

theorem HCPolySupport.HighContrast.isHermitian_lowerRight {d : ℕ} {H : BlockMat d} (hsymm : IsSymmetricBlockMat H) : Matrix.IsHermitian H.lowerRight

The lower-right block of a symmetric doubled block matrix is Hermitian.

theorem HCPolySupport.HighContrast.posSemidef_lowerRight {d : ℕ} {H : BlockMat d} (hsymm : IsSymmetricBlockMat H) (hpos : Book.Ch02.BlockPosDef H) : Matrix.PosSemidef H.lowerRight

The lower-right block of a symmetric positive definite doubled block matrix is positive semidefinite.

theorem HCPolySupport.HighContrast.isUnit_det_lowerRight {d : ℕ} {H : BlockMat d} (hpos : Book.Ch02.BlockPosDef H) : IsUnit (Matrix.det H.lowerRight)

The lower-right block of a positive definite doubled block matrix is invertible.

theorem HCPolySupport.HighContrast.schurSigmaStar_inv {d : ℕ} (H : BlockMat d) (hdet : IsUnit (Matrix.det H.lowerRight)) : (schurSigmaStar H)⁻¹ = H.lowerRight

The conjugating matrix is the inverse square root of the Schur block: the lower-right block is σ_*⁻¹, so matSqrt H.lowerRight is σ_*^{-1/2}.

theorem HCPolySupport.HighContrast.blockContrast_eq_sInf_conj {d : ℕ} {H : BlockMat d} (hsymm : IsSymmetricBlockMat H) (hpos : Book.Ch02.BlockPosDef H) : blockContrast H = sInf ((fun (h : Mat d) => specBound (matSqrt H.lowerRight * skewCorrectedForm H h * matSqrt H.lowerRight)) '' {h : Mat d | IsSkewMat h})

The intrinsic contrast in printed form. On a symmetric positive definite doubled block matrix the Loewner-scaling infimum is the infimum over skew h of the conjugated norms |σ_*^{-1/2} (σ + (k - h)ᵗ σ_*⁻¹ (k - h)) σ_*^{-1/2}|; the conjugating matrix is the positive semidefinite square root of σ_*⁻¹ = H.lowerRight.