Geodesic

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

Synchronous lattice geodesics

This file defines the graph of sup-adjacent lattice sites and the synchronous geodesic between two sites: an adjacency path whose length is the sup distance and which stays inside every centered triadic cube containing both endpoints.

def Algsuperdiff.Section5.Percolation.latticeGraph (d : ℕ) : SimpleGraph (Site d)

The simple graph whose edges are sup-adjacent lattice sites.

Equations

• Algsuperdiff.Section5.Percolation.latticeGraph d = { Adj := Algsuperdiff.Section5.Percolation.Adj, symm := ⋯, loopless := ⋯ }

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

The point reached after n synchronous sup-geodesic steps from x toward y.

Equations

• Algsuperdiff.Section5.Percolation.geodesicPoint x y n i = x i + (y i - x i).sign * ↑(n.min (y i - x i).natAbs)

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

The synchronous sup-geodesic from x to y, including both endpoints.

Equations

• Algsuperdiff.Section5.Percolation.geodesic x y = List.map (Algsuperdiff.Section5.Percolation.geodesicPoint x y) (List.range (Algsuperdiff.Section5.Percolation.siteDist x y + 1))

theorem Algsuperdiff.Section5.Percolation.geodesicPoint_mem_latticeCubeSites {d L : ℕ} {v x y : Site d} (hx : x ∈ latticeCubeSites L v) (hy : y ∈ latticeCubeSites L v) (n : ℕ) : geodesicPoint x y n ∈ latticeCubeSites L v

Every point of the synchronous geodesic between two cube sites remains in the same cube.

@[simp]

theorem Algsuperdiff.Section5.Percolation.geodesicPoint_zero {d : ℕ} (x y : Site d) : geodesicPoint x y 0 = x

The synchronous geodesic begins at its first endpoint.

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

After the sup distance many steps, the synchronous geodesic has reached its second endpoint.

@[simp]

theorem Algsuperdiff.Section5.Percolation.length_geodesic {d : ℕ} (x y : Site d) : (geodesic x y).length = siteDist x y + 1

The synchronous geodesic has one more vertex than the sup distance.

@[simp]

theorem Algsuperdiff.Section5.Percolation.headOption_geodesic {d : ℕ} (x y : Site d) : (geodesic x y).head? = some x

The synchronous geodesic starts at x.

@[simp]

theorem Algsuperdiff.Section5.Percolation.lastOption_geodesic {d : ℕ} (x y : Site d) : (geodesic x y).getLast? = some y

The synchronous geodesic ends at y.

theorem Algsuperdiff.Section5.Percolation.adj_geodesicPoint_succ {d : ℕ} (x y : Site d) {n : ℕ} (hn : n < siteDist x y) : Adj (geodesicPoint x y n) (geodesicPoint x y (n + 1))

Consecutive synchronous geodesic points are sup-adjacent until the second endpoint is reached.

theorem Algsuperdiff.Section5.Percolation.isPath_geodesic {d : ℕ} (x y : Site d) : IsPath (geodesic x y)

The synchronous geodesic is a lattice path.

theorem Algsuperdiff.Section5.Percolation.mem_latticeCubeSites_of_mem_geodesic {d L : ℕ} {v x y z : Site d} (hx : x ∈ latticeCubeSites L v) (hy : y ∈ latticeCubeSites L v) (hz : z ∈ geodesic x y) : z ∈ latticeCubeSites L v

Every vertex of a geodesic between two sites of one triadic cube belongs to that cube.

theorem Algsuperdiff.Section5.Percolation.siteDist_le_three_pow_of_mem_latticeCubeSites {d L : ℕ} {v x y : Site d} (hx : x ∈ latticeCubeSites L v) (hy : y ∈ latticeCubeSites L v) : siteDist x y ≤ 3 ^ L

The sup distance between two sites of one scale-L cube is at most 3^L.