Lattice

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

Lattice paths for the percolation estimate

This file defines the integer lattice with the sup distance, nearest-neighbor paths, centered triadic lattice cubes, and paths crossing consecutive cubes. The main geometric results are the lower bound on the number of vertices in a crossing path and the passage from the source's notion of a path, whose steps have sup distance at most one, to a path of strictly adjacent sites.

@[reducible, inline]

abbrev Algsuperdiff.Section5.Percolation.Site (d : ℕ) : Type

The integer lattice in dimension d.

Equations

• Algsuperdiff.Section5.Percolation.Site d = (Fin d → ℤ)

def Algsuperdiff.Section5.Percolation.siteDist {d : ℕ} (x y : Site d) : ℕ

The integer-valued sup distance on lattice sites.

Equations

• Algsuperdiff.Section5.Percolation.siteDist x y = Finset.univ.sup fun (i : Fin d) => (x i - y i).natAbs

theorem Algsuperdiff.Section5.Percolation.natAbs_sub_le_siteDist {d : ℕ} (x y : Site d) (i : Fin d) : (x i - y i).natAbs ≤ siteDist x y

A coordinate difference is bounded by the sup distance.

@[simp]

theorem Algsuperdiff.Section5.Percolation.siteDist_self {d : ℕ} (x : Site d) : siteDist x x = 0

The lattice sup distance vanishes on the diagonal.

theorem Algsuperdiff.Section5.Percolation.siteDist_eq_zero_iff {d : ℕ} {x y : Site d} : siteDist x y = 0 ↔ x = y

The lattice sup distance vanishes only on the diagonal.

theorem Algsuperdiff.Section5.Percolation.siteDist_comm {d : ℕ} (x y : Site d) : siteDist x y = siteDist y x

The lattice sup distance is symmetric.

theorem Algsuperdiff.Section5.Percolation.siteDist_triangle {d : ℕ} (x y z : Site d) : siteDist x z ≤ siteDist x y + siteDist y z

The lattice sup distance satisfies the triangle inequality.

def Algsuperdiff.Section5.Percolation.Adj {d : ℕ} (x y : Site d) : Prop

Two sites are adjacent when their sup distance is one. The source allows a step of sup distance at most one, hence allows a path to repeat a site; the two readings describe the same events, because deleting the repetitions of a source path changes neither its endpoints nor its vertex set; that deletion is exists_isPathFrom_of_isWeakPath.

Equations

• Algsuperdiff.Section5.Percolation.Adj x y = (Algsuperdiff.Section5.Percolation.siteDist x y = 1)

def Algsuperdiff.Section5.Percolation.IsPath {d : ℕ} (Γ : List (Site d)) : Prop

A lattice path is a finite sequence of adjacent sites.

Equations

• Algsuperdiff.Section5.Percolation.IsPath Γ = List.IsChain Algsuperdiff.Section5.Percolation.Adj Γ

def Algsuperdiff.Section5.Percolation.inCube {d : ℕ} (k : ℕ) (x : Site d) : Prop

Membership in the centered open triadic cube of scale k.

Equations

• Algsuperdiff.Section5.Percolation.inCube k x = ∀ (i : Fin d), 2 * (x i).natAbs < 3 ^ k

def Algsuperdiff.Section5.Percolation.IsPathFrom {d : ℕ} (k : ℕ) : List (Site d) → Prop

A path crossing from the scale-k cube to the complement of the scale-k+1 cube. The pattern match makes nonemptiness explicit while recording the source's head and last-vertex conditions.

Equations

• One or more equations did not get rendered due to their size.
• Algsuperdiff.Section5.Percolation.IsPathFrom k [] = False

theorem Algsuperdiff.Section5.Percolation.IsPathFrom.length_lower_bound {d k : ℕ} {Γ : List (Site d)} (hΓ : IsPathFrom k Γ) : 3 ^ k + 1 ≤ Γ.length

Any path crossing two consecutive centered triadic cubes has at least 3^k + 1 vertices.

def Algsuperdiff.Section5.Percolation.IsWeakPath {d : ℕ} (Γ : List (Site d)) : Prop

The source's notion of a path: a finite sequence of sites whose consecutive entries are at sup distance at most one, so that a site may be repeated.

Equations

• Algsuperdiff.Section5.Percolation.IsWeakPath Γ = List.IsChain (fun (x y : Algsuperdiff.Section5.Percolation.Site d) => Algsuperdiff.Section5.Percolation.siteDist x y ≤ 1) Γ

theorem Algsuperdiff.Section5.Percolation.exists_isPath_of_isWeakPath {d : ℕ} (Γ : List (Site d)) (hΓ : IsWeakPath Γ) : ∃ (Δ : List (Site d)), IsPath Δ ∧ Δ.head? = Γ.head? ∧ Δ.getLast? = Γ.getLast? ∧ Δ.toFinset = Γ.toFinset

theorem Algsuperdiff.Section5.Percolation.exists_isPathFrom_of_isWeakPath {d k : ℕ} {x y : Site d} {Γ : List (Site d)} (hΓ : IsWeakPath Γ) (hhead : Γ.head? = some x) (hlast : Γ.getLast? = some y) (hx : inCube k x) (hy : ¬inCube (k + 1) y) : ∃ (Δ : List (Site d)), IsPathFrom k Δ ∧ Δ.toFinset = Γ.toFinset