GoodCubeCrossing #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Good cubes met by a crossing of the annulus #
The chains-of-good-cubes estimate counts the sites of a crossing of the annulus
between □_{m-1} and the complement of □_m at which the event
Q(z + □_n, ε) occurs. It reads a crossing as a function x : ℕ → ℤ^d on
{0, …, N} and counts with qSiteCount, while the pre-exit cube trace of a
continuous path is a list of strictly adjacent sites whose good vertices are
counted with Finset.filter. This file converts the first count into the
second at the crossing index (m - n).toNat of the lattice 3^{n-1} ℤ^d, and
carries the resulting bound to the trace of a continuous path stopped on
leaving □_m.
Main definitions #
goodSites,goodSiteEnum— the good sites of a centered lattice cube and their injective enumeration.
Main results #
rescaledLatticePoint_eq_paperLatticePoint— the two embeddings of the site lattice3^{n-1} ℤ^dintoℝ^dagree.le_card_filter_of_isPathFrom— the good-site count along a list crossing in the discrete reading of the annulus.natThreshold_le_card_filter_of_isPathFrom— the same bound with the threshold(3/4) 3^{m-n}read as a natural number.exists_preExit_goodCubeTrace— a pre-exit cube trace of a continuous path crossing□_{n+k+1}whose good-vertex count is within2 dof the count available along every crossing of the discrete annulus at indexk.inCube_of_mem_cubeSet_partitionCube— a scale-ncell meeting□_{n+k+1}is indexed by a site of the centered cube of indexk + 1, so the trace vertices are enumerated bygoodSiteEnum.
1. The two embeddings of the site lattice #
The embedding z ↦ 3^{n-1} z used by the good cube events is the embedding
used by the path estimate.
2. From the crossing count to the good-vertex count #
The good-vertex count along a list crossing. The crossing bound
supplied for the functional reading of a crossing of the annulus at index
(m - n).toNat bounds the number of good vertices of every list crossing at
the same index.
The good-vertex count with a natural-number threshold. This is the form the trace of a continuous path consumes.
3. The pre-exit cube trace at a general threshold #
A pre-exit cube trace with the crossing count of its scale. A path
starting in the closed cube □_{n+k} and leaving □_{n+k+1} in finite
positive time has a uniformly sampled scale-n cube trace, all of whose
vertices are visited strictly before the exit, with at least L - 2 d good
vertices whenever every crossing of the discrete annulus at index k has at
least L of them. The two vertices lost are the endpoint corrections that
turn the trace into a crossing; neither of them is claimed to be visited.
4. The trace vertices, and their enumeration #
A scale-n cell that meets □_{n+k+1} is indexed by a site of the
centered cube of index k + 1. The cell of a site with
2 |z i| = 3^{k+1} + 1 already lies outside, and both sides being integers with
3^{k+1} odd, the strict inequality 2 |z i| < 3^{k+1} follows by parity.
The good sites of the centered lattice cube of index k.
Equations
Instances For
An injective enumeration of the good sites of the centered lattice cube of
index k.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Every good site of the centered lattice cube of index k is enumerated.