SiteFamilyFive #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The scale decomposition of the event Q at a lattice site #
Section 5.2 of ABK26 applies the abstract percolation path bound on the rescaled
lattice 3^{n-1} ℤ^d ↦ ℤ^d, to a family of bad events indexed by a site z and
a scale L. This module defines that family and proves the two properties that
do not involve any probability: the family covers the complement of the event
Q(3^{n-1} z + □_n, ε), and every one of its members is an event of the shells
of index at most n + L on the closed cube of its own site.
The event Q(y + □_n, ε) is the intersection of the good cube event at
y + □_n with the large-scale event 𝒥(y + □_n, Cinj⁻¹ ε γ^{-1/2}), whose
defining sum runs over every shell of index at least n. The good cube event is
an event of the cube itself; the large-scale sum is not, and this is why it is
resolved shell by shell:
B_0(z) = 𝒢(3^{n-1} z + □_n, ε)^c ∪ { shell n exceeds C_0 ε γ^{-1/2} } ,
B_L(z) = { shell n + L exceeds C_0 ε γ^{-1/2} · 3^{-L/8} } , L ≥ 1 .
The two disclosed constants #
- The threshold decay
δ = 1/8(shellDecayBase). The thresholds must be summable, and the shell tail they produce carries the exponent2 (1 - γ - δ), which the path bound needs to exceed1. Both hold withδ = 1/8throughout the rangeγ ≤ 1/4of the scaling parameter, where2 (1 - γ - δ) ≥ 5/4. - The threshold constant
C_0(siteThresholdConst). The geometric sum of the thresholds isC_0 (1 - 3^{-1/8})^{-1} ε γ^{-1/2}, so the scale decomposition needsC_0 ≤ Cinj⁻¹ (1 - 3^{-1/8}), andsiteThresholdConst Cinjis that largest admissible value.
Main definitions #
largeScaleShellTerm— thek-th term3^{(2-γ)n} ‖∇ j_k‖_{W^{1,∞}(y+□_n)}of the large-scale sum ony + □_n.shellDecayBase,shellThreshold,siteThresholdConst— the thresholds.shellExcessEvent,siteBadEventFive— the eventsB_L(z).
Main results #
mem_largeScaleEvent_iff_tsum— the large-scale event as a series over the shells above the cube scale.compl_qEvent_subset_iUnion_siteBadEventFive— the scale decomposition.measurableSet_goodCubeEvent— measurability of the good cube event in the sample, with no hypothesis beyond the model.measurableSet_siteBadEventFive_local,measurableSet_siteBadEventFive— the locality and the measurability of every member of the family.
References #
- ABK26, the event
Qand the chains of good cubes of Section 5.2.
1. The closed cube as a sup ball, and the rescaled lattice point #
2. The terms of the large-scale sum on one cube #
The k-th term of the large-scale sum on the cube y + □_n, namely
3^{(2-γ) n} ‖∇ j_k‖_{W^{1,∞}(y+□_n)}, realized by translating the shell.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The scales k ≥ n of the large-scale sum, enumerated as k = n + L.
Equations
Instances For
The large-scale event as a series over the shells above the cube scale.
3. The shell thresholds #
The geometric ratio 3^{-1/8} of the shell thresholds: the decay exponent
of the scale-resolved thresholds is δ = 1/8.
Equations
- Algsuperdiff.Section5.Support.shellDecayBase = 3 ^ (-(1 / 8))
Instances For
The powers of the ratio are the printed decay 3^{-L/8}.
The threshold of the scale-L shell event:
C_0 ε γ^{-1/2} 3^{-L/8}.
Equations
- Algsuperdiff.Section5.Support.shellThreshold M C0 ep L = C0 * ep * (√M.gamma)⁻¹ * Algsuperdiff.Section5.Support.shellDecayBase ^ L
Instances For
The admissible constant C_0(d) of the scale decomposition: the
geometric sum of the thresholds is then exactly the threshold Cinj⁻¹ ε γ^{-1/2}
of the large-scale event.
Equations
Instances For
4. The site-indexed bad events #
The scale-L shell event at the lattice site z: the shell of index
n + L contributes more than its threshold to the large-scale sum on the cube
3^{n-1} z + □_n.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The site-indexed bad events of the scale decomposition. At level 0
the good cube event at the rescaled site fails, or the shell of index n
already exceeds its threshold; at level L + 1 the shell of index n + L + 1
exceeds its threshold.
Equations
- One or more equations did not get rendered due to their size.
- Algsuperdiff.Section5.Support.siteBadEventFive M Creg C0 ep n L.succ = fun (z : Algsuperdiff.Section5.Percolation.Site d) => Algsuperdiff.Section5.Support.shellExcessEvent M C0 ep n (L + 1) z
Instances For
The threshold sum. If every shell stays below its threshold then the
whole large-scale sum on the cube stays below C_0 (1 - 3^{-1/8})^{-1} ε γ^{-1/2}.
The scale decomposition of the event Q: if the constant C_0 is small
enough that the geometric sum of the thresholds is at most the threshold
Cinj⁻¹ ε γ^{-1/2} of the large-scale event, then the complement of
Q(3^{n-1} z + □_n, ε) is covered by the site-indexed bad events.
6. Measurability of the site-indexed bad events #
The good cube event is measurable in the sample, with no hypothesis beyond the model: it is the intersection of two sublevel sets of the localized quantities, which are measurable in the sample.
The shell term of the cube y + □_n reads only the shell k on the
closed cube.
The scale-L shell event is an event of the shell n + L on the closed
cube of its own site.
Every site-indexed bad event is local: the level-L event of the site
z is an event of the shells of index at most n + L on any region containing
the closed cube 3^{n-1} z + □_n.