High-contrast homogenization: Provider.Recurrence.ColourSeparation

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

Colour separation for adapted cells

The finite-range averaging lemma colours an aligned adapted cell 3^j 𝐪 w + ⋄_j^𝐪 by the residue of its index w = 3^{-j}𝐪^{-1}z modulo three. The purpose of the rounded-grid design is that two distinct cells of the same colour are separated in ℓ^∞-distance by at least one, which is what makes the unit-range assumption applicable to them.

Two quantitative facts carry that conclusion. The first is that a rounded grid is uniformly positive: the normalization 𝓛(m) is at least the identity and the rounding perturbs the quadratic form by at most d 3^{-ℓ} ≤ 1/101, so 𝐪 ≥ (100/101) I. Consequently the grid map cannot contract the sup norm by more than the factor (100/101)/d. The second is that at any scale at or above the alignment the cells are large: 3^j ≥ 3^{k_0(d)} ≥ 101 d, this being the content of the choice of k_0(d). Two same-colour indices differ by at least three in some coordinate, so the corresponding points of the two cells differ by more than 2 · 3^j in that coordinate before the grid map is applied, and by at least 200 after it.

The colour classes themselves need no new carrier: the residue map w ↦ (w i mod 3)_i takes values in (ZMod 3)^d, so a finite family of aligned indices splits into at most 3^d same-colour classes, the count the printed proof uses.

The rounded grid is uniformly positive

theorem HCPolySupport.HighContrast.Recurrence.dotProduct_mulVec_roundedGrid_ge {d : ℕ} {l : ℤ} (hl : ↑(kZero d) ≤ l) {m : Mat d} (hm : Matrix.PosDef m) (x : Vec d) : 100 / 101 * ∑ i : Fin d, x i * x i ≤ x ⬝ᵥ Matrix.mulVec (roundedGrid l m) x

A rounded grid is at least 100/101 times the identity. The normalization is at least the identity and the rounding error moves the quadratic form by at most d 3^{-ℓ}, which kZero_spec bounds by 1/101.

theorem HCPolySupport.HighContrast.Recurrence.dotProduct_mulVec_ge_of_isRoundedGrid {d : ℕ} {l : ℤ} {q : Mat d} (hq : IsRoundedGrid l q) (x : Vec d) : 100 / 101 * ∑ i : Fin d, x i * x i ≤ x ⬝ᵥ Matrix.mulVec q x

A rounded adapted grid is at least 100/101 times the identity.

The grid map does not contract the sup norm

theorem HCPolySupport.HighContrast.Recurrence.norm_matVecMul_ge_of_isRoundedGrid {d : ℕ} {l : ℤ} {q : Mat d} (hq : IsRoundedGrid l q) (x : Vec d) : 100 / 101 * ‖x‖ ≤ ↑d * ‖matVecMul q x‖

The grid map of a rounded adapted grid does not contract the sup norm by more than d · 101/100. This is the quantitative form of positivity that the colour separation consumes.

The cells are large above the alignment

theorem HCPolySupport.HighContrast.Recurrence.mul_le_zpow_three_of_isRoundedGrid {d : ℕ} {l : ℤ} {q : Mat d} (hq : IsRoundedGrid l q) {j : ℤ} (hj : l ≤ j) : 101 * ↑d ≤ 3 ^ j

3^j ≥ 101 d at every scale at or above the alignment of a rounded grid. This is the second use of kZero_spec, and it is what makes the ℓ^∞-separation of same-colour cells at least one rather than merely positive.

Same-colour cells are unit separated

theorem HCPolySupport.HighContrast.Recurrence.unitSeparated_adaptedCellAt_of_dvd_sub {d : ℕ} {l : ℤ} {q : Mat d} (hq : IsRoundedGrid l q) {j : ℤ} (hj : l ≤ j) {w w' : Fin d → ℤ} {i₀ : Fin d} (hne : w i₀ ≠ w' i₀) (hdvd : 3 ∣ w i₀ - w' i₀) : UnitSeparated (adaptedCellAt q j w) (adaptedCellAt q j w')

Two aligned adapted cells 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 200; the printed statement asks only for one.

theorem HCPolySupport.HighContrast.Recurrence.unitSeparated_adaptedCellAt_of_intCast_eq {d : ℕ} {l : ℤ} {q : Mat d} (hq : IsRoundedGrid l q) {j : ℤ} (hj : l ≤ j) {w w' : Fin d → ℤ} (hne : w ≠ w') (hcol : (fun (i : Fin d) => ↑(w i)) = fun (i : Fin d) => ↑(w' i)) : UnitSeparated (adaptedCellAt q j w) (adaptedCellAt q j w')

Distinct same-colour aligned adapted cells are ℓ^∞-separated by at least one. The colour is the residue of the index modulo three, the index being 3^{-j}𝐪^{-1}z for the cell centred at z.

The colour classes

theorem HCPolySupport.HighContrast.Recurrence.card_image_intCast_le {d : ℕ} (Z : Finset (Fin d → ℤ)) : (Finset.image (fun (w : Fin d → ℤ) (i : Fin d) => ↑(w i)) Z).card ≤ 3 ^ d

A finite family of aligned indices meets at most 3^d colours. This is the bound K ≤ 3^d of the printed proof.

theorem HCPolySupport.HighContrast.Recurrence.biUnion_filter_intCast_eq {d : ℕ} (Z : Finset (Fin d → ℤ)) : ((Finset.image (fun (w : Fin d → ℤ) (i : Fin d) => ↑(w i)) Z).biUnion fun (c : Fin d → ZMod 3) => {w ∈ Z | (fun (i : Fin d) => ↑(w i)) = c}) = Z

A finite family of aligned indices is the union of its colour classes. Together with the separation of same-colour cells this is the decomposition I = I_1 ⊍ ⋯ ⊍ I_K of the printed proof.

theorem HCPolySupport.HighContrast.Recurrence.pairwiseDisjoint_filter_intCast {d : ℕ} (Z : Finset (Fin d → ℤ)) : (↑(Finset.image (fun (w : Fin d → ℤ) (i : Fin d) => ↑(w i)) Z)).PairwiseDisjoint fun (c : Fin d → ZMod 3) => {w ∈ Z | (fun (i : Fin d) => ↑(w i)) = c}

The colour classes of a finite family of aligned indices are disjoint. Together with the previous two facts this is the printed partition I = I_1 ⊍ ⋯ ⊍ I_K, in the form a sum over I is split by it.

theorem HCPolySupport.HighContrast.Recurrence.pairwise_unitSeparated_adaptedCellAt {d : ℕ} {ι : Type u_1} {l : ℤ} {q : Mat d} (hq : IsRoundedGrid l q) {j : ℤ} (hj : l ≤ j) {z : ι → Fin d → ℤ} (hinj : Function.Injective z) (hcol : ∀ (n n' : ι), (fun (i : Fin d) => ↑(z n i)) = fun (i : Fin d) => ↑(z n' i)) : Pairwise fun (n n' : ι) => UnitSeparated (adaptedCellAt q j (z n)) (adaptedCellAt q j (z n'))

The cells of a same-colour family of distinct aligned indices are pairwise ℓ^∞-separated by at least one. This is the hypothesis the joint independence of a colour class is proved from.

theorem HCPolySupport.HighContrast.Recurrence.intCast_eq_of_mem_filter {d : ℕ} {Z : Finset (Fin d → ℤ)} {c : Fin d → ZMod 3} {w w' : Fin d → ℤ} (hw : w ∈ {v ∈ Z | (fun (i : Fin d) => ↑(v i)) = c}) (hw' : w' ∈ {v ∈ Z | (fun (i : Fin d) => ↑(v i)) = c}) : (fun (i : Fin d) => ↑(w i)) = fun (i : Fin d) => ↑(w' i)

The members of one colour class of a finite family of aligned indices all carry that colour.