High-contrast homogenization: Provider.Entry.IdentityCells

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

The identity grid at nonnegative alignment

The comparison between adapted and Euclidean cubes compares the adapted grid with the Euclidean one, and the Euclidean grid is the identity witness. Two facts about that witness are needed at every nonnegative generation, below the rounding scale k_0(d) as well as above it.

The cells. The aligned cells of the identity grid are the standard aligned cubes and its cell at the origin is the centered triadic cube, so the cross-grid filling of l.two.grid.whitney reads on Euclidean cubes without any translation of dialect.

The alignment. IsRoundedGrid carries the rounding threshold k_0(d) because the rounding of a general witness is only faithful above it. For the identity witness the aligned-subdivision property of the coarse block — that a scale-j translation vector is integral — is the statement 3^j ℤ^d ⊆ ℤ^d, true at every j ≥ 0. The aligned subdivision and the annealed mean order of p.fixed.geometry.parent.child.recurrence therefore hold on the centered cubes from generation zero up, which is the range the persistence transfer's consumer obligation quantifies over.

Every standard aligned cube is moreover an integer translate of one whose center lies in the unit cube: at a nonnegative generation the center is itself integral, and at a negative one the index reduces modulo 3^{-k}. This is what lets integer stationarity be applied to the boundary layers of the comparison at every generation, however deep.

There are no definitions in this file.

The cells of the identity grid

theorem HCPolySupport.HighContrast.Entry.adaptedCellCenter_one {d : ℕ} (k : ℤ) (w : Fin d → ℤ) : adaptedCellCenter 1 k w = standardCellCenter k w

The aligned center of the identity grid is the center of the standard aligned cube.

theorem HCPolySupport.HighContrast.Entry.adaptedCellAt_one {d : ℕ} (k : ℤ) (w : Fin d → ℤ) : adaptedCellAt 1 k w = standardCell d k w

The aligned cell of the identity grid is the standard aligned cube.

theorem HCPolySupport.HighContrast.Entry.adaptedCellTranslate_one_zero {d : ℕ} (j : ℤ) : adaptedCellTranslate 1 j 0 = centeredCube d j

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

Reduction of a standard aligned cube to the unit cube

theorem HCPolySupport.HighContrast.Entry.standardCell_eq_translateSet {d : ℕ} {k : ℤ} {w u v : Fin d → ℤ} (h : ∀ (i : Fin d), ↑(w i) * 3 ^ k = ↑(u i) + ↑(v i) * 3 ^ k) : standardCell d k w = translateSet (Source.AKL.intTranslation u) (standardCell d k v)

A standard aligned cube is the integer translate of a second one as soon as their centers differ by the integer vector.

theorem HCPolySupport.HighContrast.Entry.exists_reduced_standardCell {d : ℕ} (k : ℤ) (w : Fin d → ℤ) : ∃ (u : Fin d → ℤ) (v : Fin d → ℤ), standardCell d k w = translateSet (Source.AKL.intTranslation u) (standardCell d k v) ∧ ∀ (i : Fin d), |standardCellCenter k v i| < 1

Every standard aligned cube is an integer translate of one centered in the unit cube. At a nonnegative generation the cube is an integer translate of the centered cube; at a negative one its index reduces modulo 3^{-k}, and the reduced center lies in [0,1)^d.

The aligned subdivision of the identity grid at nonnegative alignment

theorem HCPolySupport.HighContrast.Entry.exists_intVec_adaptedCellCenter_one {d : ℕ} {j : ℤ} (hj : 0 ≤ j) (w : Fin d → ℤ) : ∃ (v : Fin d → ℤ), adaptedCellCenter 1 j w = fun (i : Fin d) => ↑(v i)

The alignment clause at the identity grid. A scale-j translation vector of the identity grid is integral at every j ≥ 0: this is 3^j ℤ^d ⊆ ℤ^d, and it needs no rounding threshold.

theorem HCPolySupport.HighContrast.Entry.adaptedCellAt_one_eq_translateSet {d : ℕ} {j : ℤ} (hj : 0 ≤ j) (w : Fin d → ℤ) : ∃ (v : Fin d → ℤ), adaptedCellAt 1 j w = translateSet (Source.AKL.intTranslation v) (centeredCube d j)

The aligned cells of the identity grid at a nonnegative generation are integer translates of the centered cube.

theorem HCPolySupport.HighContrast.Entry.annealedBlock_adaptedCellAt_one {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} (hstat : IsStationaryLaw P) {j : ℤ} (hj : 0 ≤ j) (w : Fin d → ℤ) : annealedBlock P (adaptedCellAt 1 j w) = annealedBlock P (centeredCube d j)

The annealed block of an aligned identity cell at a nonnegative generation is the Euclidean mean at that generation.

theorem HCPolySupport.HighContrast.Entry.hasIntegrableCoarseBlock_adaptedCellAt_one {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} (hstat : IsStationaryLaw P) {j : ℤ} (hj : 0 ≤ j) (hint : HasIntegrableCoarseBlock P (centeredCube d j)) (w : Fin d → ℤ) : HasIntegrableCoarseBlock P (adaptedCellAt 1 j w)

The finiteness of the Euclidean mean transports to every aligned identity cell at a nonnegative generation.

theorem HCPolySupport.HighContrast.Entry.annealedBlock_centeredCube_le_of_nonneg {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hstat : IsStationaryLaw P) (hdag : CoarseEllipticityDagger P g E Ψ K S) {j p : ℤ} (hj : 0 ≤ j) (hjp : j ≤ p) : BlockMatLoewnerLE (annealedBlock P (centeredCube d p)) (annealedBlock P (centeredCube d j))

The annealed mean order of p.fixed.geometry.parent.child.recurrence on the Euclidean cubes, from generation zero up. The averaging step of the recurrence needs the rounding threshold only to know that the children's translation vectors are integral; at the identity witness they are integral from generation zero, so the order F_p ≤ F_j holds on the whole nonnegative range.

theorem HCPolySupport.HighContrast.Entry.annealedBlock_standardCell_le_centeredCube {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hstat : IsStationaryLaw P) (hdag : CoarseEllipticityDagger P g E Ψ K S) {k r : ℤ} (hk : 0 ≤ k) (hkr : k ≤ r) (w : Fin d → ℤ) : BlockMatLoewnerLE (annealedBlock P (standardCell d r w)) (annealedBlock P (centeredCube d k))

The Euclidean mean order at an arbitrary aligned center. Every standard aligned cube of a generation at or above k ≥ 0 has annealed block below the Euclidean mean F_k: integer stationarity moves the cube to the origin, and the alignment-zero mean order compares the generations. This is the bound the layers at or above the comparison generation consume.