PercolationScale #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The event Q, the light-path events, and the percolation scale #
Section 5.2 produces, for each maximal scale m, an ℕ-valued random variable
Y_m below which every rescaled lattice path from □_{m-n} to the complement
of □_{m-n+1} meets the good event Q at at least (3/4) 3^{m-n} of its
sites.
The reading is the strong one: for almost every sample a single Y_m precedes
all scales and all paths.
Y_m is defined here as a total ℕ-valued function of the sample, finite
in the sense of the source only almost surely: the defining property is
available exactly on the set of samples for which the light-path events stop
occurring, and the source asks only that this set carry full measure. The
statements about Y_m are accordingly almost-everywhere statements, and the
value off that set does not enter them; percolationScaleTotal_eq_zero_of_not
records what that value is. Nothing is hidden behind a caller hypothesis.
Measurable Y is a strengthening of the source, which asks only for a
random variable; it is stated explicitly and proved from the measurability of
the events Q.
Main definitions #
rescaledLatticePoint n z— the point3^{n-1} zofℝ^d.qEvent M Creg Cinj n z ep—𝒢(z+□_n, ε) ∩ 𝒥(z+□_n, Cinj⁻¹ ε γ^{-1/2}).qSiteCount M Creg Cinj n ep S omega— the number of sites ofSat whichQoccurs.lightQPathEvent M Creg Cinj m ep k— some path crosses from□_kto the complement of□_{k+1}meetingQat fewer than(3/4) 3^kof its sites.percolationScaleTotal M Creg Cinj m ep— the totalY_m.
References #
- ABK26, the chains of good cubes of Section 5.2.
The classical decidability instance used by the Finset.filter below. The
counted quantity does not depend on it: qSiteCount_eq_card_filter identifies
the count with the filter formed by any other instance.
Instances For
The event Q(z+□_n, ε): the good cube event at z + □_n intersected
with the large-scale event at threshold Cinj⁻¹ ε γ^{-1/2}.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The number of sites of S at which Q occurs, at cube scale n and
after the rescaling 3^{n-1} ℤ^d ↦ ℤ^d.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The count is insensitive to the decidability instance. Whatever
instance a consumer's Finset.filter carries, the resulting cardinality is the
one counted here.
The site count as a sum of indicators. This is the form in which the count is compared with a sum over the sites of a path, both here and where the percolation estimate's count meets the count of the statement.
2. The light-path events #
The light-path event at scale k: some lattice path starting in the
cube □_k and ending outside the cube □_{k+1} meets Q at fewer than
(3/4) 3^k of its sites. The rescaling 3^{n-1} ℤ^d ↦ ℤ^d at the cube scale
n = m - k turns the source's crossing of □_{m-1} to the complement of □_m
into this crossing of the unit lattice.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The path quantifier is countable. Only the restriction of a path to its
first N + 1 sites occurs in the light-path event, so the existential over
ℕ → Fin d → ℤ is a countable union over finite paths.
3. The total percolation scale #
The samples for which the light-path events eventually stop.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The percolation scale Y_m, as a total function of the sample: the least
scale beyond which no light path occurs. On the exceptional set where light
paths occur at arbitrarily large scales there is no such scale; the value there
is 0 and no statement below uses it.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The defining property, on the set where it is available.
The value on the exceptional set. Nothing is hidden: where light paths
occur at arbitrarily large scales the scale is 0. The almost-everywhere
statements below do not use this value.
4. The percolation scale almost surely #
The crossing bound of the source, almost surely. For almost every
sample and every scale n ≤ m - Y_m, every lattice path from □_{m-n} to the
complement of □_{m-n+1} meets Q at at least (3/4) 3^{m-n} of its distinct
sites.
5. Measurability #
The light-path events are measurable, given the measurability of the
events Q. The countable-union decomposition reduces the path quantifier to a
countable index, and on each finite path the count is a finite sum of
indicators.
The percolation scale is measurable. This is a disclosed strengthening
of the source, which asks only that Y_m be a random variable.