High-contrast homogenization:

Provider.PolynomialHomogenization.Root.RowSupply.GeneralAdaptedCellDoubledResponseFilling

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

Doubled-response filling of a general adapted cell

The maximal filling theorem applies to two arbitrary positive-definite grids. This module exposes the corresponding doubled-response subadditivity theorem without specializing the target to the base-rounded grid. It is the filling surface needed when a bounded residual dilation changes the target adapted cell but leaves the exact normalized-root grid used by the response rows.

theorem HCPolySupport.HighContrast.RowSupply.exists_coeffSpaceDoubledResponse_adaptedCellTranslate_le_tsum_filling {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) ∧ (∀ r < n, ∑ w ∈ Z r, (MeasureTheory.volume (adaptedCellAt q r w)).toReal / (MeasureTheory.volume (adaptedCellTranslate p j y)).toReal ≤ 6 * ↑d * √↑d * ‖p⁻¹ * q‖ * 3 ^ (r - j)) ∧ (∀ (r : ℤ), ∑ w ∈ Z r, (MeasureTheory.volume (adaptedCellAt q r w)).toReal / (MeasureTheory.volume (adaptedCellTranslate p j y)).toReal ≤ 1) ∧ ((Summable fun (i : (u : ℕ) × ↥(Z (n - ↑u))) => (MeasureTheory.volume (adaptedCellAt q (n - ↑i.fst) ↑i.snd)).toReal / (MeasureTheory.volume (adaptedCellTranslate p j y)).toReal * Transport.coeffSpaceDoubledResponse (adaptedCellAt q (n - ↑i.fst) ↑i.snd) a P Q) → Transport.coeffSpaceDoubledResponse (adaptedCellTranslate p j y) a P Q ≤ ∑' (i : (u : ℕ) × ↥(Z (n - ↑u))), (MeasureTheory.volume (adaptedCellAt q (n - ↑i.fst) ↑i.snd)).toReal / (MeasureTheory.volume (adaptedCellTranslate p j y)).toReal * Transport.coeffSpaceDoubledResponse (adaptedCellAt q (n - ↑i.fst) ↑i.snd) a P Q)

A general adapted cell is exhausted by a maximal family of cells from a second positive-definite grid. The row masses retain the exact cross-grid factor, and doubled response is subadditive over the resulting almost- everywhere partition whenever the weighted response series is summable.