Lattice

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

Lattice paths and triadic cubes for the ABK26 percolation estimates

This module sets up the purely combinatorial geometry underlying the appendix percolation estimates of ABK26, Section s.percolation.estimate.

ABK26 defines a path in ℤ^d to be a finite sequence x₀, …, x_N with dist (xᵢ, xᵢ₊₁) ≤ 1, and it uses the triadic cubes □_k = (-3^k/2, 3^k/2)^d.

Choice of metric

The paper's global convention is that dist is the Euclidean distance. Here we use instead the sup metric latDist, i.e. ℓ^∞. This is a deliberate strengthening, not a weakening:

• every Euclidean-adjacent pair of sites is sup-adjacent, so the class of paths used here contains the paper's class, and any upper bound proved here for the event "a long path of bad sites exists" bounds the paper's event as well;
• the finite-range independence hypotheses are quantified over pairs of site sets at distance greater than a threshold, and sup-separation is a stronger requirement than Euclidean separation, so the hypotheses assumed here hold whenever the paper's do.

Consequently the sup-metric statements proved downstream imply the Euclidean statements of ABK26. A further benefit is that on ℤ^d the sup distance is ℕ-valued, which keeps the whole development free of square roots.

Main definitions

• Algsuperdiff.Section3.Provider.Percolation.latDist: the ℕ-valued sup distance on the lattice Fin d → ℤ.
• Algsuperdiff.Section3.Provider.Percolation.cubeAt: the lattice points of the triadic cube z + □_k.
• Algsuperdiff.Section3.Provider.Percolation.IsLatticePath: the path predicate of ABK26, in the sup metric.

Main results

• latDist_triangle, coord_le_latDist: the metric A.
• mem_cubeAt_iff: cube membership in terms of latDist.
• IsLatticePath.latDist_start_succ_le: the sup distance to the starting site increases by at most one per step.
• exists_first_exit: a path ending outside a cube has a first exit index — the site there is outside the cube and every earlier site is inside.

References

• ABK26, s.percolation.estimate, paths, cubes, the Euclidean convention for dist.

The sup metric on the lattice

def Algsuperdiff.Section3.Provider.Percolation.latDist {d : ℕ} (x y : Fin d → ℤ) : ℕ

The sup distance between two sites of the lattice ℤ^d, valued in ℕ.

Equations

• Algsuperdiff.Section3.Provider.Percolation.latDist x y = Finset.univ.sup fun (j : Fin d) => (x j - y j).natAbs

theorem Algsuperdiff.Section3.Provider.Percolation.coord_le_latDist {d : ℕ} (x y : Fin d → ℤ) (j : Fin d) : (x j - y j).natAbs ≤ latDist x y

Each coordinate difference is bounded by the sup distance.

theorem Algsuperdiff.Section3.Provider.Percolation.latDist_le_iff {d : ℕ} {x y : Fin d → ℤ} {r : ℕ} : latDist x y ≤ r ↔ ∀ (j : Fin d), (x j - y j).natAbs ≤ r

The sup distance is bounded by r exactly when every coordinate difference is.

@[simp]

theorem Algsuperdiff.Section3.Provider.Percolation.latDist_self {d : ℕ} (x : Fin d → ℤ) : latDist x x = 0

theorem Algsuperdiff.Section3.Provider.Percolation.latDist_comm {d : ℕ} (x y : Fin d → ℤ) : latDist x y = latDist y x

The sup distance is symmetric.

theorem Algsuperdiff.Section3.Provider.Percolation.latDist_triangle {d : ℕ} (x y z : Fin d → ℤ) : latDist x z ≤ latDist x y + latDist y z

The triangle inequality for the sup distance.

Triadic cubes

def Algsuperdiff.Section3.Provider.Percolation.cubeAt {d : ℕ} (k : ℕ) (z : Fin d → ℤ) : Set (Fin d → ℤ)

The lattice points of the triadic cube z + □_k of ABK26: x lies in it exactly when 2 * |x j - z j| < 3 ^ k in every coordinate j.

Equations

• Algsuperdiff.Section3.Provider.Percolation.cubeAt k z = {x : Fin d → ℤ | ∀ (j : Fin d), 2 * (x j - z j).natAbs < 3 ^ k}

theorem Algsuperdiff.Section3.Provider.Percolation.three_pow_pos (k : ℕ) : 0 < 3 ^ k

theorem Algsuperdiff.Section3.Provider.Percolation.mem_cubeAt_iff {d k : ℕ} {z x : Fin d → ℤ} : x ∈ cubeAt k z ↔ 2 * latDist z x < 3 ^ k

Membership in a triadic cube expressed through the sup distance.

theorem Algsuperdiff.Section3.Provider.Percolation.self_mem_cubeAt {d : ℕ} (k : ℕ) (z : Fin d → ℤ) : z ∈ cubeAt k z

A cube contains its own centre.

Lattice paths

def Algsuperdiff.Section3.Provider.Percolation.IsLatticePath {d : ℕ} (x : ℕ → Fin d → ℤ) (N : ℕ) : Prop

ABK26: x 0, …, x N is a path when consecutive sites are at distance at most one; here in the sup metric (see the module docstring).

Equations

• Algsuperdiff.Section3.Provider.Percolation.IsLatticePath x N = ∀ i < N, Algsuperdiff.Section3.Provider.Percolation.latDist (x i) (x (i + 1)) ≤ 1

Truncation at the first exit from a cube

theorem Algsuperdiff.Section3.Provider.Percolation.exists_first_exit {d : ℕ} {x : ℕ → Fin d → ℤ} {N k : ℕ} {z : Fin d → ℤ} (hout : x N ∉ cubeAt k z) : ∃ M ≤ N, x M ∉ cubeAt k z ∧ ∀ i < M, x i ∈ cubeAt k z

If a path ends outside the cube z + □_k, it has a first exit index M: the site x M lies outside the cube and every earlier site lies inside.