High-contrast homogenization: Setup.Attainment

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

The minimum over the skew parameter is attained

The reference text writes the intrinsic contrast and the reference constant Λ_0 as minima over the skew matrices h (the intrinsic contrast of the reference block, e.Theta.m and e.reference.aspect.ratio), while the encodings blockContrast and bigLambdaRef are infima. This file proves that on the data where the reference text reads them — a symmetric doubled block matrix that is positive definite — the two readings agree: the infimum is attained at some skew matrix, so it is the printed minimum.

The mechanism is the classical one. On a positive definite doubled block matrix the lower-right block σ_*⁻¹ is coercive, so the correction (k - h)ᵗ σ_*⁻¹ (k - h) grows quadratically in h: the set of skew h admitting a fixed Loewner bound is bounded, and it is closed because the Loewner order is a closed condition. Cantor's intersection theorem along a sequence of thresholds decreasing to the infimum then produces a skew matrix realizing it.

Coercivity of a positive quadratic form

theorem HCPolySupport.HighContrast.exists_coercivity_of_quadratic_pos {d : ℕ} {M : Mat d} (hM : ∀ (x : Vec d), x ≠ 0 → 0 < vecDot x (matVecMul M x)) : ∃ (lam : ℝ), 0 < lam ∧ ∀ (x : Vec d), lam * vecNormSq x ≤ vecDot x (matVecMul M x)

Coercivity. A matrix whose quadratic form is positive away from the origin dominates a positive multiple of the squared length. The minimum of the quadratic form on the unit sphere, which is compact, is the constant.

The quadratic form of the skew-corrected Schur form

The admissible skew matrices form a compact set

Attainment

theorem HCPolySupport.HighContrast.exists_isSkewMat_matLoewnerLE_sInf_smul {d : ℕ} {H : BlockMat d} {N : Mat d} (hposH : ∀ (x : Vec d), x ≠ 0 → 0 < vecDot x (matVecMul H.lowerRight x)) (hcoerN : ∃ (lamN : ℝ), 0 < lamN ∧ ∀ (x : Vec d), lamN * vecNormSq x ≤ vecDot x (matVecMul N x)) : ∃ (h : Mat d), IsSkewMat h ∧ MatLoewnerLE (skewCorrectedForm H h) (sInf {t : ℝ | 0 ≤ t ∧ ∃ (h' : Mat d), IsSkewMat h' ∧ MatLoewnerLE (skewCorrectedForm H h') (t • N)} • N)

Attainment of the minimum over the skew parameter. On a doubled block matrix whose lower-right block has a positive quadratic form away from the origin, and against a coercive comparison matrix, the infimum of the admissible Loewner scalings is itself admissible: some skew matrix realizes it.

The printed minima

theorem HCPolySupport.HighContrast.quadratic_pos_lowerRight {d : ℕ} {H : BlockMat d} (hpos : Book.Ch02.BlockPosDef H) (x : Vec d) (hx : x ≠ 0) : 0 < vecDot x (matVecMul H.lowerRight x)

The lower-right block of a positive definite doubled block matrix has a positive quadratic form away from the origin.

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

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

theorem HCPolySupport.HighContrast.quadratic_pos_schurSigmaStar {d : ℕ} {H : BlockMat d} (hsymm : IsSymmetricBlockMat H) (hpos : Book.Ch02.BlockPosDef H) (x : Vec d) (hx : x ≠ 0) : 0 < vecDot x (matVecMul (schurSigmaStar H) x)

The Schur block σ_* of a symmetric positive definite doubled block matrix has a positive quadratic form away from the origin.

theorem HCPolySupport.HighContrast.matSqrt_lowerRight_spec {d : ℕ} {H : BlockMat d} (hsymm : IsSymmetricBlockMat H) (hpos : Book.Ch02.BlockPosDef H) : matTranspose (matSqrt H.lowerRight) = matSqrt H.lowerRight ∧ IsUnit (matSqrt H.lowerRight).det ∧ matSqrt H.lowerRight * schurSigmaStar H * matSqrt H.lowerRight = 1

The conjugating matrix. On a symmetric positive definite doubled block matrix the positive semidefinite square root of the lower-right block is symmetric, invertible, and conjugates σ_* to the identity: it is the inverse square root σ_*^{-1/2}.

theorem HCPolySupport.HighContrast.isLeast_bigLambdaRef {d : ℕ} {E : BlockMat d} (hpos : Book.Ch02.BlockPosDef E) : IsLeast ((fun (h : Mat d) => specBound (skewCorrectedForm E h)) '' {h : Mat d | IsSkewMat h}) (bigLambdaRef E)

Λ_0 is the printed minimum. On a positive definite reference block the infimum defining bigLambdaRef is attained: it is the least element of the family |σ_0 + (k_0 - h)ᵗ σ_{*,0}^{-1} (k_0 - h)| indexed by the skew matrices, which is the minimum written at e.reference.aspect.ratio.

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

The intrinsic contrast is the printed minimum. On a symmetric positive definite doubled block matrix the infimum defining blockContrast is attained: it is the least element of the family |σ_*^{-1/2} (σ + (k - h)ᵗ σ_*⁻¹ (k - h)) σ_*^{-1/2}| indexed by the skew matrices, which is the minimum written for the intrinsic contrast of the reference block and at e.Theta.m.

theorem HCPolySupport.HighContrast.exists_isSkewMat_bigLambdaRef_eq {d : ℕ} {E : BlockMat d} (hpos : Book.Ch02.BlockPosDef E) : ∃ (h : Mat d), IsSkewMat h ∧ bigLambdaRef E = specBound (skewCorrectedForm E h)

The reference constant Λ_0 is realized at some skew matrix.

theorem HCPolySupport.HighContrast.exists_isSkewMat_blockContrast_eq {d : ℕ} {H : BlockMat d} (hsymm : IsSymmetricBlockMat H) (hpos : Book.Ch02.BlockPosDef H) : ∃ (h : Mat d), IsSkewMat h ∧ blockContrast H = specBound (matSqrt H.lowerRight * skewCorrectedForm H h * matSqrt H.lowerRight)

The intrinsic contrast is realized at some skew matrix.