High-contrast homogenization: Entry.Annealed.ColourClasses

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

Residue colouring modulo three: separation, classwise independence, the 3^{d/2} count

The first paragraph of the printed proof (l.fixed.geometry.matrix.averaging):

Write z = 3^j q w and color the adapted cubes by the residue class of w modulo three. There are at most 3^d classes. Before applying 3^j q, distinct cubes in one class are separated by Euclidean distance at least two. By e.rounded.grid.bounds, their images have Euclidean separation at least 3^j, and hence ℓ^∞-separation at least 3^j/√d ≥ 1. The range-of-dependence assumption therefore makes the cubes in each class jointly independent.

Every constant below depends on d alone; no ellipticity constant occurs.

• exists_unique_index_of_mem_adaptedLatticeAtScale — for IsUnit q every lattice centre has a unique integer index, so the colouring of centres by w mod 3 is well posed. The index map itself is taken proof-locally by Classical.choose at the use site; no production definition is added.
• unitSeparated_adaptedCellAtCenter_of_residue_eq — the separation, stated as the UnitSeparated of HCPoly/Setup/LocalSigmaFields.lean. Source.AKL.supDist x y = ‖x - y‖ and the norm of Vec d = Fin d → ℝ is the ℓ^∞ norm, so this is exactly the printed ℓ^∞-separation.
• iIndepFun_coarseBlockNormalized_of_unitSeparated — classwise joint independence, from the full-matrix iIndepFun_of_coeffSigma_measurable, pushed through the fixed measurable map M ↦ S (M - A) S. The full-matrix export is used, not the fixed-entry consumer, which would give independence one entry at a time.
• sum_rpow_card_fiber_le and card_residue_colours — the class-size estimate ∑_c (#C_c)^{1/2} ≤ 3^{d/2} (#Z)^{1/2} by Cauchy-Schwarz over at most 3^d classes. Empty classes contribute 0 to both sides and are not excluded by a hypothesis.

Lattice indexing

theorem HCPolySupport.HighContrast.Annealed.exists_unique_index_of_mem_adaptedLatticeAtScale {d : ℕ} {q : Mat d} (hq : IsUnit q) (j : ℤ) {z : Vec d} (hz : z ∈ adaptedLatticeAtScale q j) : ∃! w : Fin d → ℤ, adaptedCellCenter q j w = z

For an invertible q the index of a lattice centre is unique (Geometry.adaptedCellCenter_injective), so colouring a centre by the residue of its index is well posed. The index map is produced proof-locally by Classical.choose on this statement.

Elementary norm comparisons on Vec d

theorem HCPolySupport.HighContrast.Annealed.quarter_vecNormSq_le_vecNormSq_roundedGrid_mulVec {d jStar : ℕ} {m : Mat d} (hj : 2 * d ≤ 3 ^ jStar) (hm : Matrix.PosDef m) (v : Vec d) : vecNormSq v / 4 ≤ vecNormSq (matVecMul (Geometry.explicitRoundedGrid jStar m) v)

q does not contract by more than a factor two, in the Euclidean norm: this is the printed use of e.rounded.grid.bounds's q ≥ ½ Id, through Cauchy-Schwarz and the symmetry of q.

Separation inside one colour class

theorem HCPolySupport.HighContrast.Annealed.unitSeparated_adaptedCellAtCenter_of_residue_eq {d jStar : ℕ} {m : Mat d} (hd : 2 ≤ d) (hj : 2 * d ≤ 3 ^ jStar) (hm : Matrix.PosDef m) {j : ℤ} (hjgen : ↑jStar ≤ j) {w w' : Fin d → ℤ} (hne : w ≠ w') (hres : ∀ (i : Fin d), ↑(w i) = ↑(w' i)) : UnitSeparated (adaptedCellAtCenter (Geometry.explicitRoundedGrid jStar m) j w) (adaptedCellAtCenter (Geometry.explicitRoundedGrid jStar m) j w')

Separation. Two distinct indices with the same residue modulo three give UnitSeparated adapted cells, for q = 𝒬(𝔪), 3^{j_*} ≥ 2d, d ≥ 2 and j ≥ j_*.

Route: some coordinate of w - w' has absolute value at least three, so the standard cells are ℓ^∞-separated by more than 2·3^j; q ≥ ½ Id with the symmetry of q contracts the Euclidean norm by at most a factor two; and ‖·‖_∞ ≥ ‖·‖₂/√d with 3^j ≥ 3^{j_*} ≥ 2d closes it.

Classwise joint independence

theorem HCPolySupport.HighContrast.Annealed.iIndepFun_coarseBlockNormalized_of_unitSeparated {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (hunit : IsUnitRangeLaw P) (q : Mat d) (hq : IsUnit q) (j : ℤ) {ι : Type u_1} (y : ι → Vec d) (hsep : Pairwise fun (i i' : ι) => UnitSeparated (adaptedCellTranslate q j (y i)) (adaptedCellTranslate q j (y i'))) (A R : BlockMat d) : ProbabilityTheory.iIndepFun (fun (i : ι) (a : CoeffSpace d) => toFullBlockMat (normalizedBlock (blockSub (coarseBlock (adaptedCellTranslate q j (y i)) a) A) R)) P

Classwise joint independence. A family of adapted cells that is pairwise UnitSeparated gives a jointly independent family of normalized centered blocks.

This instantiates the full-matrix iIndepFun_of_coeffSigma_measurable, giving independence of the entire family at once rather than one entry at a time.

The colour partition and its size estimate

theorem HCPolySupport.HighContrast.Annealed.card_residue_colours {d : ℕ} : Fintype.card (Fin d → ZMod 3) = 3 ^ d

There are exactly 3^d residue colours, so at most 3^d nonempty classes.

theorem HCPolySupport.HighContrast.Annealed.sum_rpow_card_fiber_le {ι : Type u_1} {κ : Type u_2} [Fintype κ] [DecidableEq κ] (Z : Finset ι) (col : ι → κ) : ∑ c : κ, ↑{z ∈ Z | col z = c}.card ^ (1 / 2) ≤ ↑(Fintype.card κ) ^ (1 / 2) * ↑Z.card ^ (1 / 2)

The class-size estimate. For any colouring of a finite set Z by a finite palette, ∑_c (#C_c)^{1/2} ≤ (#palette)^{1/2} (#Z)^{1/2}, by Cauchy-Schwarz. Empty classes contribute 0 to both sides; no nonemptiness hypothesis is used. With the palette Fin d → ZMod 3 and card_residue_colours this is the printed ∑_C (#C)^{1/2} ≤ 3^{d/2}(#Z)^{1/2}.