High-contrast homogenization: Provider.Response.DiagonalWeakNormRecentCell

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

The coarse-block term on recent scales

The difference between the child optimizer average and the parent optimizer average is controlled by the normalized child/parent coarse-block defect.

theorem HCPolySupport.HighContrast.Response.diagonalWeak_recent_cell_bound {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (k t : ℤ) {S m : Mat d} (hsymm : matTranspose S = S) (hsq : S * S = m) (hm : Matrix.PosDef m) {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) (a : CoeffSpace d) (p r : Vec d) : (blockAvsumL2 (alignedIndex q k t) fun (w : Fin d → ℤ) => blockMatVecMul (Book.Ch02.blockDiag S S⁻¹) (blockCellAverage (adaptedCellAt q k w) (diagonalWeakChildState hq k w a p r) - blockCellAverage (adaptedCell q t) (diagonalWeakState hq t a p r))) ≤ diagonalWeakMetricFactor m E * diagonalWeakLoadMinus E p r * diagonalWeakCellDefect q k t E a

The normalized square sum of child-optimizer average differences is bounded by the recent cell defect.