SiteFamilyFiveIndep #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Separated independence of the site family of Section 5.2 #
The abstract percolation path bound consumes a family B : ℕ → Site d → Set Ω
through three properties: measurability, a per-site tail bound, and the
separated independence SepIndep, which asks that blocks of sites at lattice
sup distance more than 3^l carry independent information of the levels at most
l. This module supplies the third one for the scale decomposition of the
event Q, from the finite range of dependence of the field alone.
The scale shift #
The level-L event of a site reads the shell of index n + L on the cube
3^{n-1} z + □_n, so the independence available is the one the cutoff range
lemma provides, at the Euclidean separation sqrt(d) · 3^{n+L}. What the
percolation layer supplies is the lattice separation 3^L, and the cubes
3^{n-1} z + □_n have side 3^n, three times the lattice spacing 3^{n-1}:
they overlap, and a lattice separation D only yields the Euclidean separation
3^{n-1} (D - 3). The family is therefore indexed with the same explicit scale
shift sepShift d = d that the Section 3 site family uses:
shiftedSiteBadEventFive … l z = ∅ for l < sepShift d,
= siteBadEventFive … (l - sepShift d) z otherwise.
The shift buys the factor 3^{d-1} ≥ sqrt(d) + 1, which is exactly what the
overlap costs (sqrt_add_one_le_three_pow_pred), and it changes neither the
union over the levels (badSet_shiftedSiteBadEventFive) nor any event of the
family. It costs a fixed d-dependent factor in the tail parameter and nothing
else.
Main definitions #
shiftedSiteBadEventFive— the family as the path bound indexes it.siteRegionFive— the spatial region read by a set of sites.sitePathExponent— the exponenta = 5/4of the path bound.
References #
- ABK26, the chains of good cubes of Section 5.2 and the general percolation bound of the appendix.
7. The shifted family and the observation region #
The shifted site family. The levels below the scale shift are empty;
from the shift on, the level-l event is the level-l - sepShift d bad event
of the site. The shift is what turns the lattice separation 3^l supplied by
the percolation layer into the Euclidean separation demanded by the finite range
of dependence of the field; it changes neither the union over the levels nor any
event of the family.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The shift loses nothing: the union over the shifted levels is the union over the levels of the scale decomposition.
The scale decomposition, in the form the percolation layer consumes: off
the union of the shifted bad events, the event Q of the site occurs.
The spatial region read by the whole family at the sites of Z.
Equations
Instances For
8. The separation conversion #
The dimensional slack of the scale shift. The shift sepShift d = d
buys the factor 3^{d-1} ≥ sqrt(d) + 1, which is what the overlap of the cubes
3^{n-1} z + □_n (side 3^n on a lattice of spacing 3^{n-1}) costs.
The separation conversion. Two sites at lattice sup distance more than
3^l, with l at least the scale shift, carry closed cubes at Euclidean
distance at least sqrt(d) 3^{n + l - sepShift d}, the literal cutoff range of
the shells that the events of level at most l read.
The overlap of the cubes is what the shift pays for: the cube 3^{n-1} z + □_n
has side 3^n, three times the lattice spacing 3^{n-1}, so a lattice
separation D only yields a Euclidean separation 3^{n-1}(D - 3).
9. The two-block separated independence #
The sigma-field bridge. Everything the shifted family at the sites of
Z carries up to level l is local information of the shells of index at most
n + l - sepShift d in the region read by those sites.
The two-block separated independence of the shifted family. Nothing is
assumed: two blocks of sites at lattice sup distance more than 3^l generate
local information on two regions whose Euclidean separation exceeds the literal
cutoff range of the shells they read, and the proved cutoff range lemma supplies
the independence.
The separated independence hypothesis of the path bound, discharged.
10. The exponent at which the family is fed to the path bound #
The exponent a = 5/4 at which the family is fed to the path bound.
The printed value a = 2 - γ is not attainable: summability of the thresholds
and the shell tail force a < 2 (1 - γ), and with the decay exponent δ = 1/8
of shellDecayBase the largest admissible exponent at γ = 1/4 is exactly
2 (1 - γ - δ) = 5/4.
Equations
Instances For
The path bound's dimension gate a ≤ d holds in every dimension of the
model.
The exponent and the threshold decay are consistent. The shell tail
produced by the threshold C_0 ε γ^{-1/2} 3^{-L/8} carries the exponent
2 (1 - γ - 1/8), which is at least a = 5/4 throughout the range of the
scaling parameter.