HitExitBridge

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

From visited partition cubes to hit-exit chaining

This file supplies the geometric and counting interface required by the hit-then-exit argument. A finite injective enumeration lists the relevant scale-n lattice sites. Its closed cells are padded by the empty set to a family indexed by ℕ; its open enlargements have the same centers and three times the side length. At most 3^d closed cells meet any one enlargement.

def Algsuperdiff.Section5.Trace.closedPartitionCube {d : ℕ} (n : ℤ) (z : Percolation.Site d) : Set (HCPolySupport.Vec d)

The closed scale-n cell centered at the embedded lattice site z.

Equations

• Algsuperdiff.Section5.Trace.closedPartitionCube n z = Metric.closedBall (Algsuperdiff.Section5.Trace.rescaleSite n z) (1 / 2 * 3 ^ n)

def Algsuperdiff.Section5.Trace.openEnlargedPartitionCube {d : ℕ} (n : ℤ) (z : Percolation.Site d) : Set (HCPolySupport.Vec d)

The open enlargement of a scale-n cell, with the same center and side length 3^(n+1).

Equations

• Algsuperdiff.Section5.Trace.openEnlargedPartitionCube n z = Metric.ball (Algsuperdiff.Section5.Trace.rescaleSite n z) (3 / 2 * 3 ^ n)

theorem Algsuperdiff.Section5.Trace.cubeSet_partitionCube_subset_closedPartitionCube {d : ℕ} (n : ℤ) (z : Percolation.Site d) : HCPolySupport.cubeSet (partitionCube n z) ⊆ closedPartitionCube n z

The half-open partition representative lies in its closed cell.

def Algsuperdiff.Section5.Trace.neighboringSites {d : ℕ} (v : Percolation.Site d) : Finset (Percolation.Site d)

The finite neighborhood containing all coordinatewise unit offsets of a site.

Equations

• Algsuperdiff.Section5.Trace.neighboringSites v = Finset.image (fun (delta : Algsuperdiff.Section5.Percolation.Site d) => v + delta) (Algsuperdiff.Section5.Percolation.cubeSites d 1)

theorem Algsuperdiff.Section5.Trace.siteDist_le_one_of_closedPartitionCube_inter_openEnlarged_nonempty {d : ℕ} (n : ℤ) {z v : Percolation.Site d} (hinter : (closedPartitionCube n z ∩ openEnlargedPartitionCube n v).Nonempty) : Percolation.siteDist z v ≤ 1

If a closed scale-n cell meets the open threefold enlargement of another cell, their lattice sites differ by at most one in every coordinate.

def Algsuperdiff.Section5.Trace.enumeratedClosedCubeFamily {d r : ℕ} (n : ℤ) (sites : Fin r ↪ Percolation.Site d) (i : ℕ) : Set (HCPolySupport.Vec d)

A finite injective site enumeration, padded by empty sets, as closed hit sets for the chaining theorem.

Equations

• Algsuperdiff.Section5.Trace.enumeratedClosedCubeFamily n sites i = if hi : i < r then Algsuperdiff.Section5.Trace.closedPartitionCube n (sites ⟨i, hi⟩) else ∅

def Algsuperdiff.Section5.Trace.enumeratedOpenEnlargementFamily {d r : ℕ} (n : ℤ) (sites : Fin r ↪ Percolation.Site d) (i : ℕ) : Set (HCPolySupport.Vec d)

The corresponding padded family of open threefold enlargements.

Equations

• Algsuperdiff.Section5.Trace.enumeratedOpenEnlargementFamily n sites i = if hi : i < r then Algsuperdiff.Section5.Trace.openEnlargedPartitionCube n (sites ⟨i, hi⟩) else ∅

theorem Algsuperdiff.Section5.Trace.isOpen_enumeratedOpenEnlargementFamily {d r : ℕ} (n : ℤ) (sites : Fin r ↪ Percolation.Site d) (i : ℕ) : IsOpen (enumeratedOpenEnlargementFamily n sites i)

Every padded enlargement is open.

theorem Algsuperdiff.Section5.Trace.enumeratedCubeFamily_overlap {d r : ℕ} (n : ℤ) (sites : Fin r ↪ Percolation.Site d) (i : ℕ) : ∃ (s : Finset ℕ), s.card ≤ 3 ^ d ∧ ∀ (j : ℕ), (enumeratedClosedCubeFamily n sites j ∩ enumeratedOpenEnlargementFamily n sites i).Nonempty → j ∈ s

For an injective enumeration, each open enlargement meets at most 3^d members of the padded closed-cell family.