LatticeBridge

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

Two readings of a crossing of the annulus □_k → □_{k+1}^c

A crossing of the lattice annulus is written in two ways in this development.

• As a function x : ℕ → Fin d → ℤ together with a length N, with consecutive sites at sup distance at most one (IsLatticePath), starting in the cube □_k and ending outside □_{k+1}. This is the reading of the source: a step may stay put, so a site may be repeated.
• As a list Γ : List (Fin d → ℤ) of strictly adjacent sites with the same endpoint conditions (IsPathFrom k). This is the reading of the percolation path estimate.

The two readings describe the same crossings once the count attached to a crossing is a count of distinct sites: deleting the repetitions of a functional crossing changes neither its endpoints nor its set of sites. This file proves that equivalence, and records the geometric consequence that a crossing visits at least 3 ^ k + 2 distinct sites.

Main definitions

• pathSites N x — the set of sites visited by x on {0, …, N}.

Main results

• exists_isPathFrom_of_isLatticePath, exists_isLatticePath_of_isPathFrom — the two directions of the translation, each preserving the set of sites.
• exists_crossing_iff — the resulting equivalence for any property of the set of sites.

References

• ABK26, the percolation estimate for bad cubes.

1. The two lattices agree

theorem Algsuperdiff.Section5.Percolation.siteDist_eq_latDist {d : ℕ} (x y : Site d) : siteDist x y = Section3.Provider.Percolation.latDist x y

The two sup distances on the lattice are the same function.

theorem Algsuperdiff.Section5.Percolation.inCube_iff_mem_cubeAt {d k : ℕ} {x : Site d} : inCube k x ↔ x ∈ Section3.Provider.Percolation.cubeAt k 0

Membership in the centred cube agrees with membership in the cube at the origin.

2. The sites of a functional crossing

def Algsuperdiff.Section5.Percolation.pathSites {d : ℕ} (N : ℕ) (x : ℕ → Site d) : Finset (Site d)

The set of sites visited by x on {0, …, N}.

Equations

• Algsuperdiff.Section5.Percolation.pathSites N x = Finset.image x (Finset.range (N + 1))

theorem Algsuperdiff.Section5.Percolation.mem_pathSites {d N : ℕ} {x : ℕ → Site d} {z : Site d} : z ∈ pathSites N x ↔ ∃ i ≤ N, x i = z

3. From a functional crossing to a list crossing

theorem Algsuperdiff.Section5.Percolation.exists_isPathFrom_of_isLatticePath {d k N : ℕ} {x : ℕ → Site d} (hpath : Section3.Provider.Percolation.IsLatticePath x N) (h0 : x 0 ∈ Section3.Provider.Percolation.cubeAt k 0) (hN : x N ∉ Section3.Provider.Percolation.cubeAt (k + 1) 0) : ∃ (Γ : List (Site d)), IsPathFrom k Γ ∧ Γ.toFinset = pathSites N x

4. From a list crossing to a functional crossing

theorem Algsuperdiff.Section5.Percolation.exists_isLatticePath_of_isPathFrom {d k : ℕ} {Γ : List (Site d)} (hΓ : IsPathFrom k Γ) : ∃ (N : ℕ) (x : ℕ → Site d), Section3.Provider.Percolation.IsLatticePath x N ∧ x 0 ∈ Section3.Provider.Percolation.cubeAt k 0 ∧ x N ∉ Section3.Provider.Percolation.cubeAt (k + 1) 0 ∧ pathSites N x = Γ.toFinset

theorem Algsuperdiff.Section5.Percolation.exists_crossing_iff {d : ℕ} (k : ℕ) (P : Finset (Site d) → Prop) : (∃ (N : ℕ) (x : ℕ → Site d), Section3.Provider.Percolation.IsLatticePath x N ∧ x 0 ∈ Section3.Provider.Percolation.cubeAt k 0 ∧ x N ∉ Section3.Provider.Percolation.cubeAt (k + 1) 0 ∧ P (pathSites N x)) ↔ ∃ (Γ : List (Site d)), IsPathFrom k Γ ∧ P Γ.toFinset

The two readings of a crossing agree, for any property of the set of sites visited.