High-contrast homogenization:

Provider.PolynomialHomogenization.Root.RowSupply.GeneralAdaptedCellDoubledResponseAggregation

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

Row-majorant aggregation on a general adapted-cell filling

The response bound produced by the general filling is aggregated here against one nonnegative majorant per exact-grid row. This is the form consumed by a power-tail response certificate after translation, dilation, and gauge have identified its exact-grid cell responses.

theorem HCPolySupport.HighContrast.RowSupply.exists_coeffSpaceDoubledResponse_adaptedCellTranslate_le_tsum_rowMajorant {d : ℕ} [NeZero d] {p q : Mat d} (hp : Matrix.PosDef p) (hq : Matrix.PosDef q) (n j : ℤ) (y : Vec d) (a : CoeffSpace d) (P Q : BlockVec d) : ∃ (Z : ℤ → Finset (Fin d → ℤ)), (∀ (r : ℤ), ↑(Z r) = Transport.fillingIndex q n (adaptedCellTranslate p j y) r) ∧ ∀ (B : ℤ → ℝ), (∀ (r : ℤ), 0 ≤ B r) → (∀ (u : ℕ), ∀ w ∈ Z (n - ↑u), Book.Ch02.doubledResponseJ (Response.adaptedDomainAt hq (n - ↑u) w) (a.coeffOn (Response.adaptedDomainAt hq (n - ↑u) w)) P Q ≤ B (n - ↑u)) → (Summable fun (u : ℕ) => (if u = 0 then 1 else 6 * ↑d * √↑d * ‖p⁻¹ * q‖ * 3 ^ (n - ↑u - j)) * B (n - ↑u)) → Transport.coeffSpaceDoubledResponse (adaptedCellTranslate p j y) a P Q ≤ ∑' (u : ℕ), (if u = 0 then 1 else 6 * ↑d * √↑d * ‖p⁻¹ * q‖ * 3 ^ (n - ↑u - j)) * B (n - ↑u)

A summable rowwise majorant on the filling grid controls doubled response on an arbitrary adapted target. The top row pays one and lower rows pay the exact cross-grid boundary factor.