Documentation

LeanPool.HighContrastHomogenization.Provider.Quenched.FixedGridWindowScale

High-contrast homogenization: Provider.Quenched.FixedGridWindowScale #

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

Scale account for a fixed canonical grid #

A fixed rounded grid whose witness eccentricity is bounded by the reference aspect ratio fits in a dimensionally enlarged centered cube. The enlargement is linear in the logarithmic reference scale, so a fixed four-generation response lag fits inside a coupled source window with a dimensional execution coefficient.

source
noncomputable def HCPolySupport.HighContrast.Quenched.canonicalGridEnlargement (d : ℕ) (Pi : ℝ) :
ℕ

The number of extra triadic generations needed to enclose a rounded grid whose witness eccentricity is at most Pi.

Equations
Instances For
    source
    theorem HCPolySupport.HighContrast.Quenched.norm_roundedGrid_mul_sqrt_le_canonicalGridEnlargement {d : ℕ} (hd : 2 ≤ d) {l : ℤ} (hl : ↑(kZero d) ≤ l) {m : Mat d} (hm : Matrix.PosDef m) {Pi : ℝ} (hPi : 1 ≤ Pi) (hecc : witnessEccentricity m ≤ Pi) :
    ‖roundedGrid l m‖ * √↑d ≤ 3 ^ canonicalGridEnlargement d Pi

    Rounding at any admissible fixed scale preserves the canonical enclosure bound.