OnePointChainTrace #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The early-exit bound for a process read inside a larger carrier #
The chaining input of the early-exit bound is a cube trace: almost every path leaving the maximal
cube in finite time visits, strictly before that exit, at least D distinct good scale-n cells.
The trace is produced by a deterministic argument about continuous paths of the state space.
Here the process lives on a larger carrier, the state space being read inside it by an open
embedding, and the paths are paths of the carrier. Two facts bridge the gap. A path that never
leaves the read state space is the reading of a path of the state space itself, so the
deterministic trace argument applies to it verbatim; and the exit time from a read set, along a
read path, is the exit time from the set itself. The chaining estimate is then applied on the
carrier, at the read cube families of OnePointChainPath.
The hypothesis that the paths stay in the read state space is explicit. For the compactified process of a conservative live semigroup it is the almost-sure liveness of the paths.
Main results #
exists_goodCubeTrace_of_eval_zero— the deterministic pre-exit trace at a fixed starting point.ae_exists_goodCubeTrace_image— its almost-sure form for a process of the carrier.measure_exitTime_le_le_rho_pow_of_good_cube_trace_image— the hit-then-exit estimate for the read families.measure_exitTime_le_le_rho_pow_of_percolation_crossing_image— the early-exit bound at one sample and one scale, on the carrier.
References #
- ABK26, the chaining of Section 5.3.
1. The deterministic pre-exit trace #
The pre-exit good cube trace at a fixed starting point. A continuous path starting in the
closed cube □_{n+k} and leaving □_{n+k+1} in finite time has a scale-n cube trace, all of
whose vertices are visited strictly before the exit, with at least L - 2 d good vertices, each
enumerated by goodSiteEnum (k + 1).
2. The trace along a path of the carrier #
The trace hypothesis on the carrier. Almost every path of the read process that leaves the read maximal cube in finite time has a read cube trace with the same count. The two inputs are that the paths stay in the read state space and that they start where the process is started.
The read family of visited cells. Distinct good sites of a read cube trace give the finite set of distinct family indices the chaining estimate consumes.
3. The hit-then-exit estimate on the carrier #
Trace-to-tail consumer bridge on a carrier. The read padded cells satisfy the counting
hypothesis of the hit-then-exit estimate and their read threefold enlargements the overlap
hypothesis with K = 3^d, so the estimate gives Q_x(τ ≤ t) ≤ exp(lam t) rho^N whenever
N 3^d < D.
4. The early-exit bound at one sample and one scale #
The early-exit bound from one crossing count, on the carrier. This is the estimate of
measure_exitTime_le_le_rho_pow_of_percolation_crossing for a process of a carrier in which the
state space is read by an open embedding, with the almost-sure confinement of the paths to the
read state space as the one extra input.