High-contrast homogenization: Provider.PolynomialHomogenization.NormalizedBlockPositivity

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

Positivity of constant comparison blocks

The full block matrix associated with a coefficient matrix is positive definite as soon as the coefficient's symmetric part is positive definite. The reflected block then gives the inverse action needed to calibrate the primal and dual response loads.

theorem HCPolySupport.HighContrast.blockPosDef_constantBlockMatrix_of_posDef_symmPart {d : ℕ} {a0 : Mat d} (hS : Matrix.PosDef (symmPart a0)) : Book.Ch02.BlockPosDef (Book.Ch02.constantBlockMatrix a0)

The constant comparison block is positive definite whenever the symmetric part of its coefficient matrix is positive definite.

theorem HCPolySupport.HighContrast.blockMatVecMul_constantBlockMatrix_blockReflect_inv_of_posDef_symmPart {d : ℕ} {a0 : Mat d} (hS : Matrix.PosDef (symmPart a0)) (Y : BlockVec d) : blockMatVecMul (Book.Ch02.constantBlockMatrix a0) (blockMatVecMul (blockReflect (Book.Ch02.constantBlockMatrix a0)) Y) = Y

Applying a constant block after its reflected block recovers the input.