High-contrast homogenization: Provider.PolynomialHomogenization.AdaptedCellExcessQuenchedRow

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

Adapted-cell excesses from a shifted quenched row

An aligned adapted child is first filled by standard cells. If its parent adapted cell lies in an enlarged centered cube, the resulting boundary convolution is controlled by the quenched block row at that enlarged scale.

theorem HCPolySupport.HighContrast.blockExcess_coarseBlock_adaptedCellAt_le_quenched_block_row {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) (t n G : ℕ) (a : CoeffSpace d) (abar : Mat d) (habar : Matrix.PosDef (symmPart abar)) (rho sourceScale : ℝ) (hrho : 0 < rho) (hrho1 : rho ≤ 1) (henclose : adaptedCell q ↑t ⊆ centeredCube d ↑(t + G)) (hactive : sourceScale ≤ 3 ^ (t + G)) (w : Fin d → ℤ) (hw : w ∈ Response.alignedIndex q (↑t - ↑n) ↑t) : blockExcess (coarseBlock (adaptedCellAt q (↑t - ↑n) w) a) (Book.Ch02.constantBlockMatrix abar) ≤ max 1 (6 * ↑d * √↑d * ‖q⁻¹‖) * 3 ^ (rho * ↑(n + G)) * Quenched.quenchedBlockRow rho (Book.Ch02.constantBlockMatrix abar) sourceScale a (t + G)

A standard-cell quenched row on a centered enlargement controls the excess of every aligned adapted child. The shift records both the depth of the child and the fixed enlargement of its parent.