High-contrast homogenization: Provider.Quenched.UnitRangeCellSeparation

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

Colour separation of the standard aligned cubes

The concentration-for-sums condition supplied by unit range of dependence is a statement about a family of observables indexed by the standard aligned cubes z + □_n, z ∈ 3^n ℤ^d ∩ □_m, of e.coarse.ellipticity. Neighbouring cubes of that family touch, so unit range does not apply to the family as a whole. It applies after a triadic colouring: two distinct cubes of the same scale whose indices agree modulo three are separated in ℓ^∞-distance by more than one, so the local sigma-fields they carry are independent.

This file records that geometry for the standard cubes, in the two forms the concentration argument consumes: measurability of the cubes, and pairwise unit separation of a same-colour family. The colour classes need no new carrier: the residue map w ↦ (w i mod 3)_i takes values in (ZMod 3)^d, and the partition of a finite index family into its colour classes is the one already used by the finite-range averaging estimate.

The standard aligned cubes are measurable

theorem HCPolySupport.HighContrast.Quenched.measurableSet_standardCell (d : ℕ) (k : ℤ) (w : Fin d → ℤ) : MeasurableSet (standardCell d k w)

A standard aligned cube is a measurable subset of ℝ^d.

Same-colour cubes are unit separated

theorem HCPolySupport.HighContrast.Quenched.unitSeparated_standardCell_of_dvd_sub {d : ℕ} {k : ℤ} (hk : 0 ≤ k) {w w' : Fin d → ℤ} {i₀ : Fin d} (hne : w i₀ ≠ w' i₀) (hdvd : 3 ∣ w i₀ - w' i₀) : UnitSeparated (standardCell d k w) (standardCell d k w')

Two standard aligned cubes at a nonnegative scale whose indices differ by a nonzero multiple of three in some coordinate are ℓ^∞-separated by at least one. In fact they are separated by at least two; the unit-range assumption asks only for one.

theorem HCPolySupport.HighContrast.Quenched.unitSeparated_standardCell_of_intCast_eq {d : ℕ} {k : ℤ} (hk : 0 ≤ k) {w w' : Fin d → ℤ} (hne : w ≠ w') (hcol : (fun (i : Fin d) => ↑(w i)) = fun (i : Fin d) => ↑(w' i)) : UnitSeparated (standardCell d k w) (standardCell d k w')

Two distinct standard aligned cubes of the same colour are ℓ^∞-separated by at least one. The colour of a cube is the residue of its index modulo three.