High-contrast homogenization: Provider.PolynomialHomogenization.AdaptedCellExcessFilling

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

Excess domination through an adapted-cell filling

The maximal filling of one adapted cell by cells of another grid is an exhaustion in both doubled orientations. Consequently, a uniform bound on the weighted excess of every finite set of filling rows passes to the coarse block of the target cell. This is the deterministic boundary-layer step used when a cube response row is compared with a response row on an adapted grid.

theorem HCPolySupport.HighContrast.blockExcess_coarseBlock_adaptedCellTranslate_le_of_filling_rows {d : ℕ} [NeZero d] {p q : Mat d} (hp : Matrix.PosDef p) (hq : Matrix.PosDef q) {n j : ℤ} {y : Vec d} {Z : ℤ → Finset (Fin d → ℤ)} (hZ : ∀ (r : ℤ), ↑(Z r) = Transport.fillingIndex q n (adaptedCellTranslate p j y) r) {F : BlockMat d} (hF : IsSymmetricBlockMat F) (hFpd : Book.Ch02.BlockPosDef F) (a : CoeffSpace d) {E : ℝ} (hE : 0 ≤ E) (hrows : ∀ J ≤ n, ∑ r ∈ Finset.Icc J n, ∑ w ∈ Z r, (MeasureTheory.volume (adaptedCellAt q r w)).toReal / (MeasureTheory.volume (adaptedCellTranslate p j y)).toReal * blockExcess (coarseBlock (adaptedCellAt q r w) a) F ≤ E) : blockExcess (coarseBlock (adaptedCellTranslate p j y) a) F ≤ E

If every finite collection of rows in a maximal filling has weighted cell excess at most E, then the target cell has excess at most E. The same cell excess controls the reflected response, so the exhaustion is supplied in both orientations without a second hypothesis.