Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section3.Provider.Percolation.BadClusters

BadClusters #

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

l.percolation.bad.clusters: the density and diameter conclusions #

This module feeds the site family of SiteFamilyBridge.lean and the per-scale tails of SiteFamilyTails.lean into the abstract percolation layer, at the gates of BadClusterRate.lean, and produces the two displayed conclusions of ABK26's Lemma l.percolation.bad.clusters.

The admissibility interfaces #

The original public compatibility theorems carry the amended display e.percolation.admissibility.bad.clusters:

E >= exp(C sigma^{-1}) ,   E >= C c_star^{-1} ,   E >= C b^{-1} ,   gamma <= E^{-5} ,

The standing source hypotheses E in [1,infinity), S(m-1,E), sigma in (0,1/2], b in (0,1/8] and h in N (with h >= 1, the manuscript's N convention) are carried verbatim.

The corresponding declarations suffixed _of_gates expose instead the four raw consequences actually used by the single-cube probability estimates: 4 <= E, unitGate M, gamma <= 1/20, and E⁻² <= cstar. This separates the probabilistic proof from the stronger packaged premise and lets the frozen maximum gate discharge the exact consequences directly.

The density conclusion #

e.density.bound.bad.clusters:

P[ avsum_{z in 3^{m-h} Z^d cap cu_m} 1_{B^*(z + cu_{m-h})}
     > exp(-c E^{-2} gamma^{-1}) + 3^{-h/2} ]  <=  exp(-3^{h/2}) .

Proved locally as measureReal_badExtendedDensity_gt_le_exp_of_gates, with the explicit dimension-only c(d) = siteRateBase d / 2. The threshold's first term is supplied by the tail sum of the site family; the deviation half is measureReal_densityAverage_gt_le_exp, whose range binder is verified by densityThreshold_of_le at the gate densityAmplitude_le_sqrt_siteRateSq. The manuscript's own a = 3/2 forces d >= 2 (the source lemma's own a < d); this is the disclosed constraint.

The diameter conclusion #

e.diameter.bound.bad.clusters is the probability that some 2-cluster of B^*_{m-h} has diameter at least 3^{bh} 3^{m-h}. What the percolation layer supplies, and what is proved here, is the probabilistic content of that display: the union over the base lattice 3^{m-h} Z^d cap cu_m of the crossing events of e.diameter.bound at the scale k = ceil(b h) has probability at most exp(-3^{(1-sigma) b h}) (measureReal_badClusterCrossingEvent_le_exp). The entropy-versus-gain step is exactly the arithmetic, discharged by entropyGate_of_admissible.

Main results #

References #

Elementary numerics #

The tail sum of the site family #

source
theorem Algsuperdiff.Section3.Provider.Percolation.measureReal_badUnion_siteBadEvent_le_of_gates {d : ℕ} (M : ABKModel d) (base : ℤ) {m : ℤ} {E : ℝ} (hE : 1 ≤ E) (hE4 : 4 ≤ E) (hunit : BadEvents.unitGate M) (hgamma20 : M.gamma ≤ 1 / 20) (hinvSq : E⁻¹ ^ 2 ≤ Disorder.cstar M) (hS : Frozen.Section3.inductionState M (m - 1) ⟨E, hE⟩) (hbase : base ≤ m - 1) (hgamma : M.gamma ≤ E ^ (-5)) (hEabs : 2 * (Real.log 20 + 9 * ↑d * Real.log 3) ≤ BadEvents.badRateConst d * E ^ 3) (hrate : 4 ≤ siteRateSq M E) (u : Fin d → ℤ) :
(↑(Cutoff.cutoffSampleLaw M)).real (badUnion (siteBadEvent M base) u) ≤ Real.exp (-(siteRateSq M E / 2))

The probability of the extended bad event's superset. The union over all reindexed levels of the site family — the abstract layer's B(z) — has probability at most exp(-c(d) E^{-2} gamma^{-1}) with c(d) = siteRateBase d / 2. This is the first term of the threshold in e.density.bound.bad.clusters.

The density statistic of e.bad.cluster.def #

source
noncomputable def Algsuperdiff.Section3.Provider.Percolation.badExtendedDensity {d : ℕ} (M : ABKModel d) (m : ℤ) (h : ℕ) :
Cutoff.CutoffSample d → ℝ

ABK26 e.bad.cluster.def: the normalized count of those base cubes z + cu_{m-h}, z in 3^{m-h} Z^d cap cu_m, for which the extended bad event `B^*(z

  • cu_{m-h})occurs. The lattice3^{m-h} Z^d cap cu_mis represented by `cubeFinset hthroughz = 3^{m-h} u`.
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Algsuperdiff.Section3.Provider.Percolation.badExtendedDensity_le_densityAverage_add {d : ℕ} (M : ABKModel d) (m : ℤ) (h : ℕ) {theta : ℝ} (hp : ∀ (u : Fin d → ℤ), (↑(Cutoff.cutoffSampleLaw M)).real (badUnion (siteBadEvent M (m - ↑h)) u) ≤ theta) (omega : Cutoff.CutoffSample d) :
    badExtendedDensity M m h omega ≤ densityAverage (siteBadEvent M (m - ↑h)) (↑(Cutoff.cutoffSampleLaw M)) h omega + theta

    The manuscript's own inclusion B^* subseteq bigcup_L B_L, at the level of the density statistic: the extended-bad density is dominated by the centered density average of the site family plus the uniform bound on the centering.

    The density conclusion #

    source
    theorem Algsuperdiff.Section3.Provider.Percolation.measureReal_badExtendedDensity_gt_le_exp_of_gates {d : ℕ} (M : ABKModel d) {m : ℤ} (h : ℕ) {E sigma b : ℝ} (hd : 2 ≤ d) (hh : 1 ≤ h) (hE : 1 ≤ E) (hS : Frozen.Section3.inductionState M (m - 1) ⟨E, hE⟩) (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) (hb0 : 0 < b) (hb1 : b ≤ 1 / 8) (hEexp : Real.exp (badClustersConst d / sigma) ≤ E) (hE4 : 4 ≤ E) (hunit : BadEvents.unitGate M) (hgamma20 : M.gamma ≤ 1 / 20) (hinvSq : E⁻¹ ^ 2 ≤ Disorder.cstar M) (hEb : badClustersConst d / b ≤ E) (hgamma : M.gamma ≤ E ^ (-5)) :
    (↑(Cutoff.cutoffSampleLaw M)).real {omega : Cutoff.CutoffSample d | Real.exp (-(siteRateBase d / 2 * (E⁻¹ ^ 2 * M.gamma⁻¹))) + 3 ^ (-↑h / 2) < badExtendedDensity M m h omega} ≤ Real.exp (-3 ^ (↑h / 2))

    ABK26 e.density.bound.bad.clusters, at the explicit dimension-only constant c(d) = siteRateBase d / 2 and from the raw single-cube probability gates.

    P[ avsum_{z} 1_{B^*(z + cu_{m-h})} > exp(-c E^{-2} gamma^{-1}) + 3^{-h/2} ]
  <= exp(-3^{h/2}) .

    The range binder of measureReal_densityAverage_gt_le_exp is verified inside, at the manuscript's own a = 3/2; the source lemma's own constraint a < d forces the disclosed d >= 2.

    The diameter conclusion #