PercolationAssembly

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

The crossing bridge for the chains of good cubes

Section 5.2 asserts that, for every maximal scale m, there is an integer-valued random variable Y_m with an exponential tail such that below the scale m - Y_m every rescaled lattice path crossing the annulus between the cubes □_{m-n} and □_{m-n+1} meets the good event Q(z + □_n, ε) at at least three quarters of 3^{m-n} of its sites.

One step of that argument is recorded here: the passage from a crossing that is light for the good event Q to a crossing that is light for the site-indexed family shiftedSiteBadEventFive, the family the abstract percolation path estimate is applied to. The complement of a bad site is contained in Q, so a path visiting few sites of Q visits few complements of bad sites, and the count the path estimate controls bounds qSiteCount from below.

Main results

• lightQPathEvent_subset — a light crossing of the annulus is a light crossing for the site-indexed family.

References

• ABK26, the chains of good cubes of Section 5.2.

theorem Algsuperdiff.Section5.Provider.lightQPathEvent_subset {d : ℕ} (M : Section3.ABKModel d) {Creg Cinj C0 ep : ℝ} (m : ℤ) (k : ℕ) (hC0 : 0 ≤ C0) (hep : 0 ≤ ep) (hthr : C0 * (1 - Support.shellDecayBase)⁻¹ ≤ Cinj⁻¹) : Support.lightQPathEvent M Creg Cinj m ep k ⊆ {omega : Section3.Cutoff.CutoffSample d | ∃ (Gamma : List (Percolation.Site d)), Percolation.IsPathFrom k Gamma ∧ ∑ z ∈ Gamma.toFinset, (Percolation.badSet (Support.shiftedSiteBadEventFive M Creg C0 ep (m - ↑k)) z)ᶜ.indicator (fun (x : Section3.Cutoff.CutoffSample d) => 1) omega < (1 - 1 / 4) * 3 ^ k}

A light crossing of the annulus is a light crossing for the site family. The complement of the union over scales of the bad events at a site is contained in Q at that site, so the good-vertex count of the percolation estimate is at most the count of sites at which Q occurs. The two readings of a crossing — as a function on an initial segment and as a list of adjacent sites — are identified by exists_crossing_iff, which carries the set of visited sites across unchanged.