RescaledPathBound #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The percolation path bound on the paper lattice #
The paper indexes its cube events by 3^(n-1) ℤ^d. This file embeds that
lattice in Vec d, identifies its centered crossing annulus with
Percolation.IsPathFrom (m-n), and restates Percolation.path_bound with
events evaluated at the physical lattice points.
Throughout Section 5, both path adjacency and spatial separation are measured
in the ℓ∞ metric. The equivalence below makes this explicit:
lattice site distance at most L is the same as physical sup distance at most
L * 3^(n-1).
noncomputable def
Algsuperdiff.Section5.Trace.paperLatticePoint
{d : ℕ}
(n : ℤ)
(z : Percolation.Site d)
:
The paper's embedding of ℤ^d as the lattice 3^(n-1) ℤ^d.