High-contrast homogenization: Provider.Response.PreYoungRecentDefectPointwise

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

Pointwise recent-defect pairings

The average of the child--parent optimizer difference is controlled by its half doubled-energy and the appropriate Schur load of the cell response.

theorem HCPolySupport.HighContrast.Response.abs_vec_dot_recent_difference_le {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) {s t : ℤ} (hst : s ≤ t) {w : Fin d → ℤ} (hw : w ∈ alignedIndex q s t) (a : CoeffSpace d) (p r Pcen Qcen : Vec d) : have energy := 1 / 2 * Book.Ch02.average (adaptedDomainAt hq s w) fun (x : Vec d) => blockVecDot (diagonalWeakChildState hq s w a p r x - diagonalWeakState hq t a p r x) (blockMatVecMul (blockMatrixOfCoeff (↑↑a x)) (diagonalWeakChildState hq s w a p r x - diagonalWeakState hq t a p r x)); |vecDot Qcen (blockCellAverage (adaptedCellAt q s w) fun (x : Vec d) => diagonalWeakChildState hq s w a p r x - diagonalWeakState hq t a p r x).1| ≤ √(2 * energy) * profileSchurLoadFlux (coarseBlock (adaptedCellAt q s w) a) Qcen ∧ |vecDot Pcen (blockCellAverage (adaptedCellAt q s w) fun (x : Vec d) => diagonalWeakChildState hq s w a p r x - diagonalWeakState hq t a p r x).2| ≤ √(2 * energy) * profileSchurLoadGradient (coarseBlock (adaptedCellAt q s w) a) Pcen

The two coordinate pairings of a recent child--parent difference are controlled by its half doubled-energy and the cell Schur loads.