High-contrast homogenization: Provider.PolynomialHomogenization.AdaptedCellExcessBoundary #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Boundary-row control of an adapted-cell excess #
Filling an adapted cell by Euclidean triadic cells loses one geometric boundary weight per generation. A nonnegative summable majorant for the Euclidean cell excesses therefore controls the excess of the adapted cell by its convolution with that boundary kernel.
theorem
HCPolySupport.HighContrast.blockExcess_coarseBlock_adaptedCellAt_le_boundary_tsum
{d : ℕ}
[NeZero d]
{q : Mat d}
(hq : Matrix.PosDef q)
(k : ℤ)
(z : Fin d → ℤ)
(a : CoeffSpace d)
{F : BlockMat d}
(hF : IsSymmetricBlockMat F)
(hFpd : Book.Ch02.BlockPosDef F)
(B : ℤ → ℝ)
(hB0 : ∀ (r : ℤ), 0 ≤ B r)
(hBsum : Summable fun (n : ℕ) => 3 ^ (-↑n) * B (k - ↑n))
(hcell :
∀ (r : ℤ) (w : Fin d → ℤ),
r ≤ k → standardCell d r w ⊆ adaptedCellAt q k z → blockExcess (coarseBlock (standardCell d r w) a) F ≤ B r)
:
The excess of an adapted cell is bounded by the Euclidean-cell excess
majorant convolved with the geometric boundary kernel. The hypothesis on B
is local to cells of at most the target's scale contained in the target, so a
containing Euclidean cube can be inserted later without changing this
deterministic statement.