High-contrast homogenization: Provider.Quenched.SmallContrastBootstrapIdentityGrid

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

The Euclidean grid as a rounded adapted grid

The bootstrap of the small-contrast window compares the adapted mean on the selection grid with the annealed block on a centered cube. The comparison is read through the tilt scalarization, whose reference argument is an adapted mean on a rounded grid; so the Euclidean cube must itself be presented as an adapted cell of a rounded grid.

Rounding fixes the identity witness at every nonnegative alignment: each diagonal entry rounds the integer 3^j and each off-diagonal entry is zero. The identity-grid file records this under a coupled window; the bootstrap has no window, and the statement needs none — nonnegativity of the alignment is the whole hypothesis.

theorem HCPolySupport.HighContrast.Quenched.roundedGrid_one_of_nonneg {d : ℕ} [Nonempty (Fin d)] {j : ℤ} (hj : 0 ≤ j) : roundedGrid j 1 = 1

Rounding fixes the identity witness at every nonnegative alignment. This is the window-free form of the Initialization.roundedGrid_one.

theorem HCPolySupport.HighContrast.Quenched.isRoundedGrid_one {d : ℕ} [Nonempty (Fin d)] {l : ℤ} (hl : ↑(kZero d) ≤ l) : IsRoundedGrid l 1

The Euclidean grid is a rounded adapted grid at every admissible alignment.

theorem HCPolySupport.HighContrast.Quenched.adaptedMean_one {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (m : ℤ) : adaptedMean P 1 m = annealedBlock P (centeredCube d m)

The adapted mean of the Euclidean grid is the annealed block of the centered cube.