Coloring

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Triadic lattice cubes and the separation colouring

ABK26 states its concentration corollary for a family {X_z}_{z ∈ 3^n ℤ^d ∩ □_m} whose members are independent whenever the corresponding subcubes do not touch. Turning that hypothesis into an application of the concentration inequality requires a colouring: the lattice is split into finitely many classes, each of which is pairwise separated beyond the range of dependence, the concentration inequality is applied inside each class, and the classes are recombined by the triangle inequality.

This module supplies the two purely combinatorial ingredients.

• The finite set cubeFinset m of lattice points of □_m, with cardinality 3 ^ (d * m); mem_cubeFinset_iff characterizes its members by 2 · latDist 0 x < 3 ^ m, which is what Lattice.mem_cubeAt_iff says of the set cubeAt m 0, i.e. of ABK26's □_m ∩ ℤ^d.
• The colouring siteColor L, the residue of a site modulo 3 ^ L + 1. Two distinct sites of the same colour differ by a multiple of 3 ^ L + 1 in some coordinate, hence are separated at range 3 ^ L, which is exactly the separation demanded by ABK26's finite-range hypothesis.

The recombination cost is the Cauchy--Schwarz bound sum_sqrt_card_colorClass_le, which controls ∑_c √(#class c) by √(colourCount) · √(#S). The colour count is taken to be the minimum of the number (3 ^ L + 1) ^ d of residues and the total site count #S: the second bound, valid because √n ≤ n for a nonempty class, is the sharper one once the range of dependence exceeds the diameter of the cube, and it is what keeps the scale sum of the ABK26 density bound convergent.

Main definitions

• Algsuperdiff.Section3.Provider.Percolation.cubeFinset
• Algsuperdiff.Section3.Provider.Percolation.siteColor
• Algsuperdiff.Section3.Provider.Percolation.colorClass

Main results

• card_cubeFinset, mem_cubeFinset_iff, cubeFinset_nonempty
• three_pow_lt_latDist_of_siteColor_eq: same colour and distinct implies separated at range 3 ^ L.
• sum_sqrt_card_colorClass_le: the Cauchy--Schwarz recombination cost.

References

• ABK26, triadic cubes, the concentration corollary, the finite-range hypothesis.

The lattice points of a triadic cube

def Algsuperdiff.Section3.Provider.Percolation.cubeRadius (m : ℕ) : ℕ

Half-width of the triadic cube □_m: the lattice points of □_m are those whose coordinates all lie in [-cubeRadius m, cubeRadius m].

Equations

• Algsuperdiff.Section3.Provider.Percolation.cubeRadius m = (3 ^ m - 1) / 2

theorem Algsuperdiff.Section3.Provider.Percolation.two_mul_cubeRadius_add_one (m : ℕ) : 2 * cubeRadius m + 1 = 3 ^ m

noncomputable def Algsuperdiff.Section3.Provider.Percolation.cubeFinset {d : ℕ} (m : ℕ) : Finset (Fin d → ℤ)

The lattice points of the triadic cube □_m, as a Finset.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.Percolation.mem_cubeFinset_iff {d m : ℕ} {x : Fin d → ℤ} : x ∈ cubeFinset m ↔ 2 * latDist 0 x < 3 ^ m

theorem Algsuperdiff.Section3.Provider.Percolation.cubeFinset_nonempty {d : ℕ} (m : ℕ) : (cubeFinset m).Nonempty

theorem Algsuperdiff.Section3.Provider.Percolation.card_cubeFinset {d : ℕ} (m : ℕ) : (cubeFinset m).card = 3 ^ (d * m)

The separation colouring

def Algsuperdiff.Section3.Provider.Percolation.siteColor {d : ℕ} (L : ℕ) (x : Fin d → ℤ) : Fin d → ZMod (3 ^ L + 1)

The colour of a lattice site at separation scale L: its residue modulo 3 ^ L + 1.

Equations

• Algsuperdiff.Section3.Provider.Percolation.siteColor L x j = ↑(x j)

theorem Algsuperdiff.Section3.Provider.Percolation.three_pow_lt_latDist_of_siteColor_eq {d L : ℕ} {x y : Fin d → ℤ} (hc : siteColor L x = siteColor L y) (hxy : x ≠ y) : 3 ^ L < latDist x y

Distinct sites of the same colour are separated. This is the geometric content of the colouring: it converts the colour classes into families to which ABK26's finite-range independence hypothesis at range 3 ^ L applies.

def Algsuperdiff.Section3.Provider.Percolation.colorClass {d : ℕ} (L : ℕ) (S : Finset (Fin d → ℤ)) (c : Fin d → ZMod (3 ^ L + 1)) : Finset (Fin d → ℤ)

The colour class of c inside a finite set of sites.

Equations

• Algsuperdiff.Section3.Provider.Percolation.colorClass L S c = {x ∈ S | Algsuperdiff.Section3.Provider.Percolation.siteColor L x = c}

theorem Algsuperdiff.Section3.Provider.Percolation.mem_colorClass_iff {d L : ℕ} {S : Finset (Fin d → ℤ)} {c : Fin d → ZMod (3 ^ L + 1)} {x : Fin d → ℤ} : x ∈ colorClass L S c ↔ x ∈ S ∧ siteColor L x = c

theorem Algsuperdiff.Section3.Provider.Percolation.colorClass_subset {d L : ℕ} {S : Finset (Fin d → ℤ)} {c : Fin d → ZMod (3 ^ L + 1)} : colorClass L S c ⊆ S

theorem Algsuperdiff.Section3.Provider.Percolation.colorClass_nonempty {d L : ℕ} {S : Finset (Fin d → ℤ)} {c : Fin d → ZMod (3 ^ L + 1)} (hc : c ∈ Finset.image (siteColor L) S) : (colorClass L S c).Nonempty

theorem Algsuperdiff.Section3.Provider.Percolation.three_pow_lt_latDist_of_mem_colorClass {d L : ℕ} {S : Finset (Fin d → ℤ)} {c : Fin d → ZMod (3 ^ L + 1)} {x y : Fin d → ℤ} (hx : x ∈ colorClass L S c) (hy : y ∈ colorClass L S c) (hxy : x ≠ y) : 3 ^ L < latDist x y

Sites of one colour class are pairwise separated at range 3 ^ L.

The recombination cost

theorem Algsuperdiff.Section3.Provider.Percolation.card_image_siteColor_le {d : ℕ} (L : ℕ) (S : Finset (Fin d → ℤ)) : (Finset.image (siteColor L) S).card ≤ (3 ^ L + 1) ^ d

At most (3 ^ L + 1) ^ d colours occur: the number of residue vectors modulo 3 ^ L + 1.

theorem Algsuperdiff.Section3.Provider.Percolation.sum_card_colorClass {d : ℕ} (L : ℕ) (S : Finset (Fin d → ℤ)) : ∑ c ∈ Finset.image (siteColor L) S, ↑(colorClass L S c).card = ↑S.card

theorem Algsuperdiff.Section3.Provider.Percolation.sum_sqrt_card_colorClass_le {d : ℕ} (L : ℕ) (S : Finset (Fin d → ℤ)) : ∑ c ∈ Finset.image (siteColor L) S, √↑(colorClass L S c).card ≤ √(min ↑((3 ^ L + 1) ^ d) ↑S.card) * √↑S.card

The Cauchy--Schwarz recombination cost of the colouring.

The colour count is the minimum of the number (3 ^ L + 1) ^ d of residues and the total number of sites.