High-contrast homogenization: Provider.PolynomialHomogenization.BlockExcessHomogenizationError

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

HCPolySupport error controlled by a row of block excesses

The normalized response on a cube is bounded by the excess of its coarse block over a fixed constant comparison block. Descendants of an origin cube are reindexed by standard-cell labels. A coefficient-space sample also has a single finite excess bound valid on every standard cell inside a prescribed bounded window; later weighted-row arguments may therefore establish genuine summability without choosing samplewise ellipticity constants as public data. The window is supplied by the containment of a standard cell of scale at most M, centred in the centered cube of scale M, in the centered cube of scale M + 1.

theorem HCPolySupport.HighContrast.maxDescendantNormalizedBlockResponseAtScale_originCube_eq_alignedIndex {d : ℕ} (m : ℤ) (n : ℕ) (aL : Book.Ch02.TriadicCoeffFamily d) (abar : Mat d) : Book.Ch02.maxDescendantNormalizedBlockResponseAtScale (originCube d m) (m - ↑n) aL abar = Book.Ch02.finsetSupReal (Response.alignedIndex 1 (m - ↑n) m) fun (w : Fin d → ℤ) => Book.Ch02.normalizedBlockResponseMax (translateCube w (originCube d (m - ↑n))) aL abar

Descendants of an origin cube at a fixed depth are exactly the standard cells whose centres lie in that origin cube.

theorem HCPolySupport.HighContrast.isBounded_centeredCube (d : ℕ) (M : ℤ) : Bornology.IsBounded (centeredCube d M)

Every centered triadic cube is bounded.

theorem HCPolySupport.HighContrast.standardCell_subset_centeredCube_succ {d : ℕ} {k M : ℤ} {w : Fin d → ℤ} (hw : standardCellCenter k w ∈ centeredCube d M) (hkM : k ≤ M) : standardCell d k w ⊆ centeredCube d (M + 1)

A standard cell of scale at most M whose centre lies in the centered cube of scale M lies in the centered cube of scale M + 1: the cell reaches at most its own half-width beyond its centre.

theorem HCPolySupport.HighContrast.standardCell_blockExcess_nonneg {d : ℕ} [NeZero d] (a : CoeffSpace d) {F : BlockMat d} (hF : IsSymmetricBlockMat F) (hFpd : Book.Ch02.BlockPosDef F) (k : ℤ) (w : Fin d → ℤ) : 0 ≤ blockExcess (coarseBlock (standardCell d k w) a) F

Every standard-cell excess over a symmetric positive definite comparison block is nonnegative: the coarse block of a cell is positive semidefinite.

theorem HCPolySupport.HighContrast.exists_uniform_standardCell_blockExcess_bound {d : ℕ} [NeZero d] (a : CoeffSpace d) (abar : Mat d) (habar : Matrix.PosDef (symmPart abar)) {S : Set (Vec d)} (hS : Bornology.IsBounded S) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (k : ℤ) (w : Fin d → ℤ), standardCell d k w ⊆ S → blockExcess (coarseBlock (standardCell d k w) a) (Book.Ch02.constantBlockMatrix abar) ≤ C

Every standard cell inside one bounded window admits one nonnegative finite upper bound on its excess. The bound may depend on the sample, the comparison matrix and the window, but not on the cell scale or label.