CubeTrace

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

Triadic cube traces of uniformly sampled paths

This file turns a sufficiently fine uniform sampling of a continuous path in Vec d into the weak lattice paths used by the Section 5 percolation bound.

We use Homogenization.cubeSet, the half-open realization [(z_i - 1/2) 3^n, (z_i + 1/2) 3^n), so every point belongs to the cube whose site is obtained by coordinatewise integer rounding after division by 3^n. Thus the cube site is exactly Algsuperdiff.Section5.Percolation.Site d after rescaling by 3⁻ⁿ. The predicate Percolation.inCube k is the centered open cube condition on these rescaled integer sites.

noncomputable def Algsuperdiff.Section5.Trace.nearestTriadicSite {d : ℕ} (n : ℤ) (x : HCPolySupport.Vec d) : Percolation.Site d

The site of the scale-n half-open triadic partition containing x. At boundary points, integer rounding selects the cube on the positive side.

Equations

• Algsuperdiff.Section5.Trace.nearestTriadicSite n x i = round (x i / 3 ^ n)

def Algsuperdiff.Section5.Trace.partitionCube {d : ℕ} (n : ℤ) (z : Percolation.Site d) : HCPolySupport.TriadicCube d

The scale-n triadic partition cube indexed by the lattice site z.

Equations

• Algsuperdiff.Section5.Trace.partitionCube n z = { scale := n, index := z }

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

The embedding of a lattice site as the center of its scale-n cube.

Equations

• Algsuperdiff.Section5.Trace.rescaleSite n z i = ↑(z i) * 3 ^ n

theorem Algsuperdiff.Section5.Trace.mem_partitionCube_nearestTriadicSite {d : ℕ} (n : ℤ) (x : HCPolySupport.Vec d) : x ∈ HCPolySupport.cubeSet (partitionCube n (nearestTriadicSite n x))

Coordinatewise rounding assigns every point to its half-open partition cube, including points on cube boundaries.

theorem Algsuperdiff.Section5.Trace.siteDist_nearestTriadicSite_le_one_of_dist_lt {d : ℕ} (n : ℤ) {x y : HCPolySupport.Vec d} (hxy : dist x y < 3 ^ n) : Percolation.siteDist (nearestTriadicSite n x) (nearestTriadicSite n y) ≤ 1

Points less than one scale-n side length apart in the Vec d sup metric are assigned sites at lattice sup distance at most one.

noncomputable def Algsuperdiff.Section5.Trace.cubeTrace {d M : ℕ} (n : ℤ) (point : Fin (M + 1) → HCPolySupport.Vec d) : List (Percolation.Site d)

The sequence of scale-n cube sites containing a tuple of sample points.

Equations

• Algsuperdiff.Section5.Trace.cubeTrace n point = List.ofFn fun (k : Fin (M + 1)) => Algsuperdiff.Section5.Trace.nearestTriadicSite n (point k)

theorem Algsuperdiff.Section5.Trace.cubeTrace_isWeakPath {d M : ℕ} (n : ℤ) (point : Fin (M + 1) → HCPolySupport.Vec d) (hstep : ∀ (k : ℕ) (hk : k + 1 < M + 1), dist (point ⟨k, ⋯⟩) (point ⟨k + 1, hk⟩) < 3 ^ n) : Percolation.IsWeakPath (cubeTrace n point)

A point tuple with consecutive sup distances less than 3^n has a weak lattice cube trace.

noncomputable def Algsuperdiff.Section5.Trace.uniformSampleTime (T : NNReal) (M : ℕ) (k : Fin (M + 1)) : NNReal

The time of the kth point in the uniform subdivision of [0,T] into M pieces.

Equations

• Algsuperdiff.Section5.Trace.uniformSampleTime T M k = ↑↑k * T / ↑M

noncomputable def Algsuperdiff.Section5.Trace.uniformCubeTrace {d : ℕ} (n : ℤ) (M : ℕ) (omega : MarkovProcess.ContinuousPath (HCPolySupport.Vec d)) (T : NNReal) : List (Percolation.Site d)

The cube trace of the uniform subdivision of a continuous path.

Equations

• Algsuperdiff.Section5.Trace.uniformCubeTrace n M omega T = Algsuperdiff.Section5.Trace.cubeTrace n fun (k : Fin (M + 1)) => omega (Algsuperdiff.Section5.Trace.uniformSampleTime T M k)

theorem Algsuperdiff.Section5.Trace.exists_uniformCubeTrace_lt_exitTime {d : ℕ} (U : Set (HCPolySupport.Vec d)) (omega : MarkovProcess.ContinuousPath (HCPolySupport.Vec d)) (T : NNReal) (hT : ↑T < MarkovProcess.ContinuousPath.exitTime U omega) (n : ℤ) : ∃ (M : ℕ), 0 < M ∧ (∀ (k : Fin (M + 1)), ↑(uniformSampleTime T M k) < MarkovProcess.ContinuousPath.exitTime U omega) ∧ Percolation.IsWeakPath (uniformCubeTrace n M omega T) ∧ ∀ (k : Fin (M + 1)), omega (uniformSampleTime T M k) ∈ HCPolySupport.cubeSet (partitionCube n (nearestTriadicSite n (omega (uniformSampleTime T M k))))

Uniform continuity supplies a strictly pre-exit uniform sampling whose scale-n cube trace is weakly adjacent. Every sampled point lies in its recorded half-open partition cube.