High-contrast homogenization: Provider.Window.CellGeometry #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Standard cells inside growing centered windows #
The scale and center conditions used by the bad-scale supremum follow directly from containment of a standard cell in the bounded window. These elementary facts keep the stopped-scale argument independent of a coordinate choice.
theorem
HCPolySupport.HighContrast.Window.centeredCube_mono
{d : ℕ}
{m n : ℤ}
(hmn : m ≤ n)
:
centeredCube d m ⊆ centeredCube d n
Centered triadic cubes increase with their generation.
theorem
HCPolySupport.HighContrast.Window.scale_le_of_standardCell_subset_centeredCube
{d : ℕ}
(hd : 0 < d)
{k m : ℤ}
{w : Fin d → ℤ}
(hsub : standardCell d k w ⊆ centeredCube d m)
:
A standard cell contained in a centered window cannot have larger scale than the window.
theorem
HCPolySupport.HighContrast.Window.standardCell_data_in_enlargedWindow
{d : ℕ}
(hd : 0 < d)
{k M : ℤ}
{w : Fin d → ℤ}
(hsub : standardCell d k w ⊆ centeredCube d M)
(ℓ : ℕ)
:
A cell in the original window meets the center and scale conditions of every nonnegative enlargement.