High-contrast homogenization: Provider.Initialization.IdentityGrid

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

The rounded identity grid

At the nonnegative alignment supplied by a coupled window, every diagonal entry being rounded is the integer 3^j and every off-diagonal entry is zero. Rescaling therefore returns the identity exactly.

theorem HCPolySupport.HighContrast.Initialization.centeredCube_subset_centeredCube {d : ℕ} {r M : ℤ} (hrM : r ≤ M) : centeredCube d r ⊆ centeredCube d M

Centered triadic cubes are nested with their integer scale.

theorem HCPolySupport.HighContrast.Initialization.adaptedCell_one {d : ℕ} (r : ℤ) : adaptedCell 1 r = centeredCube d r

The adapted cell of the identity grid is the centered triadic cube.

theorem HCPolySupport.HighContrast.Initialization.roundedGrid_one {d : ℕ} {Q K : ℝ} {jStar M : ℤ} [Nonempty (Fin d)] (hw : IsCoupledWindow d Q K jStar M) : roundedGrid jStar 1 = 1

The identity witness is fixed by rounding at the alignment of a coupled window.

theorem HCPolySupport.HighContrast.Initialization.identity_admissible_index {d : ℕ} {Q K : ℝ} {jStar M r : ℤ} [Nonempty (Fin d)] (hw : IsCoupledWindow d Q K jStar M) (hjr : jStar ≤ r) (hrM : r ≤ M) : IsAdmissibleIndex (roundedGrid jStar 1) jStar M r 0

Every identity-grid scale in the window range is an admissible centered index.