High-contrast homogenization: Provider.Selection.EnclosureGeometry

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

Geometry of the selection enclosure

The grids retained by the selector have exponentially controlled eccentricity. After rounding, this gives a uniform operator-norm bound and hence a fixed enlargement that places every adapted cell inside a centered triadic cube. The same enclosure contains all aligned cells whose centers lie in either terminal cell.

The grid enlargement

noncomputable def HCPolySupport.HighContrast.Selection.gridEnlargement (d : ℕ) (chop : ℝ) (Ncap : ℕ) : ℕ

The integer enlargement needed to contain every grid used by a capped selection run.

Equations

• HCPolySupport.HighContrast.Selection.gridEnlargement d chop Ncap = ⌈Real.logb 3 (√↑d * (100 / 99)) + chop * ↑(Ncap + 1) / Real.log 3⌉₊

Linear images of centered cubes

theorem HCPolySupport.HighContrast.Selection.adaptedCell_subset_centeredCube_add {d : ℕ} (hd : 1 ≤ d) {q : Mat d} {T : ℤ} {G : ℕ} (hq : ‖q‖ * √↑d ≤ 3 ^ G) : adaptedCell q T ⊆ centeredCube d (T + ↑G)

An operator-norm bound turns an adapted cell into a centered cube after a fixed integer enlargement.

theorem HCPolySupport.HighContrast.Selection.roundedGrid_adaptedCell_subset_gridEnlargement {d : ℕ} (hd : 2 ≤ d) {jdag T : ℤ} (hjdag : ↑(kZero d) ≤ jdag) {m : Mat d} (hm : Matrix.PosDef m) {chop : ℝ} {Ncap : ℕ} (hecc : witnessEccentricity m ≤ Real.exp (chop * ↑(Ncap + 1))) : adaptedCell (roundedGrid jdag m) T ⊆ centeredCube d (T + ↑(gridEnlargement d chop Ncap))

A rounded grid whose witness has the capped eccentricity bound fits in the displayed enlarged centered cube.

The enlargement budget

theorem HCPolySupport.HighContrast.Selection.gridEnlargement_le {d : ℕ} (hd : 2 ≤ d) {chop CN Lam : ℝ} (hchop : 0 ≤ chop) (hLam : 1 ≤ Lam) (Ncap : ℕ) (hcap : ↑(Ncap + 1) ≤ (CN + 3) * Lam) : ↑(gridEnlargement d chop Ncap) ≤ (2 + 1 / 2 * Real.logb 3 ↑d + chop / Real.log 3 * (CN + 3)) * Lam

The capped enlargement is bounded by the sharp coefficient used in the execution-window budget.

The terminal cell family

theorem HCPolySupport.HighContrast.Selection.adaptedCellTranslate_subset_of_mem_containedCenters {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) {k v : ℤ} (hkv : k ≤ v) {z : Vec d} (hz : z ∈ containedCenters q k v) : adaptedCellTranslate q k z ⊆ adaptedCell q v

An aligned cell whose center belongs to a larger adapted cell is contained in that cell.

theorem HCPolySupport.HighContrast.Selection.terminal_enclosure_of_adaptedCell_enclosure {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) {jdag s t Mexec : ℤ} (hjs : jdag ≤ s) (hst : s ≤ t) (hwhole : ∀ (k : ℤ), jdag ≤ k → k ≤ t → adaptedCell q k ⊆ centeredCube d Mexec) : (∀ (k : ℤ), jdag ≤ k → k ≤ t → adaptedCell q k ⊆ centeredCube d Mexec) ∧ ∀ k < jdag, ∀ (v : ℤ), v = s ∨ v = t → ∀ z ∈ containedCenters q k v, adaptedCellTranslate q k z ⊆ centeredCube d Mexec

Enclosure of the terminal adapted-cell tower implies both terminal enclosure clauses, including every aligned cell below the starting scale.