High-contrast homogenization: Provider.Response.DiagonalWeakNormRecentEnergyMap

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

The energy map for a recent optimizer difference

On a recent child the local optimizer and the restricted parent optimizer are solutions for one coefficient representative. Their doubled difference is therefore a response field, so the coarse energy-map estimate applies to its cell average.

theorem HCPolySupport.HighContrast.Response.metricBlockNormSq_recent_difference_le {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) {k t : ℤ} (hkt : k ≤ t) {w : Fin d → ℤ} (hw : w ∈ alignedIndex q k t) (a : CoeffSpace d) (p r : Vec d) {m : Mat d} (hm : Matrix.PosDef m) {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) : metricBlockNormSq m (blockCellAverage (adaptedCellAt q k w) fun (x : Vec d) => diagonalWeakChildState hq k w a p r x - diagonalWeakState hq t a p r x) ≤ diagonalWeakMetricFactor m E ^ 2 * blockSize (adaptedResponse q k w a) E * Book.Ch02.average (adaptedDomainAt hq k w) fun (x : Vec d) => blockVecDot (diagonalWeakChildState hq k w a p r x - diagonalWeakState hq t a p r x) (blockMatVecMul (blockMatrixOfCoeff (↑↑a x)) (diagonalWeakChildState hq k w a p r x - diagonalWeakState hq t a p r x))

The metric square of the averaged optimizer difference on one child is controlled by the child's response size and the actual difference energy.