Documentation

LeanPool.HighContrastHomogenization.Provider.Response.ProfileRowSchur

High-contrast homogenization: Provider.Response.ProfileRowSchur #

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

Schur estimate for an all-earlier response row #

The inverse square root of schurSigmaStar is the square root of the lower-right block. Together with the top-left block this gives the exact factor-two estimate used by the response row.

source
theorem HCPolySupport.HighContrast.Response.profileSchurLoad_nonneg {d : ℕ} (H : BlockMat d) (Pcen Qcen : Vec d) :
0 ≤ profileSchurLoad H Pcen Qcen
source
theorem HCPolySupport.HighContrast.Response.profileSchurLoad_le_two_mul_profileQuadraticLoad {d : ℕ} {H : BlockMat d} (hsymm : IsSymmetricBlockMat H) (hpos : Book.Ch02.BlockPosDef H) (Pcen Qcen : Vec d) :
profileSchurLoad H Pcen Qcen ≤ 2 * profileQuadraticLoad H Pcen Qcen

The Schur diagonal load is at most twice the sum of the two diagonal quadratic forms.

source
theorem HCPolySupport.HighContrast.Response.profileSchurLoad_adjointBlock {d : ℕ} (H : BlockMat d) (Pcen Qcen : Vec d) :
profileSchurLoad (profileAdjointBlock H) Pcen Qcen = profileSchurLoad H Pcen Qcen

Coefficient transposition leaves both diagonal Schur carriers unchanged.

source
theorem HCPolySupport.HighContrast.Response.profileQuadraticLoad_adjointBlock {d : ℕ} (H : BlockMat d) (Pcen Qcen : Vec d) :
profileQuadraticLoad (profileAdjointBlock H) Pcen Qcen = profileQuadraticLoad H Pcen Qcen

Coefficient transposition leaves the sum of diagonal quadratic forms unchanged.