Documentation

LeanPool.HighContrastHomogenization.Provider.Response.ProfileCenterPointwise

High-contrast homogenization: Provider.Response.ProfileCenterPointwise #

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

Pointwise control of terminal optimizer centers #

The optimizer-average identity turns the difference between a random terminal average and its annealed center into the block reflection of one centered response matrix. The self-dual metric comparison then bounds its length by the centered terminal maximum.

source
theorem HCPolySupport.HighContrast.Response.metricBlockNormSq_responseAverage_sub_le {d : ℕ} {m : Mat d} (hm : Matrix.PosDef m) {A E : BlockMat d} (hA : IsSymmetricBlockMat A) (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) (X : BlockVec d) :
metricBlockNormSq m (blockMatVecMul (Book.Ch02.blockR d) (blockMatVecMul A X) + X - (blockMatVecMul (Book.Ch02.blockR d) (blockMatVecMul E X) + X)) ≤ diagonalWeakMetricFactor m E ^ 2 * blockVecDot X (blockMatVecMul E X) * blockSize (blockSub A E) E ^ 2

A centered response matrix controls the reflected optimizer-average difference in the diagonal metric.

source
theorem HCPolySupport.HighContrast.Response.sqrt_metricBlockNormSq_responseAverage_sub_le {d : ℕ} {m : Mat d} (hm : Matrix.PosDef m) {A E : BlockMat d} (hA : IsSymmetricBlockMat A) (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) (p r : Vec d) :
√(metricBlockNormSq m (blockMatVecMul (Book.Ch02.blockR d) (blockMatVecMul A (-p, r)) + (-p, r) - (blockMatVecMul (Book.Ch02.blockR d) (blockMatVecMul E (-p, r)) + (-p, r)))) ≤ diagonalWeakMetricFactor m E * diagonalWeakLoadMinus E p r * blockSize (blockSub A E) E

The square-root form of the primal centered-average comparison.