SiteTails

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

Surviving elementary bounds for the site-tail construction

This module retains the logarithmic bounds, the set identity for the complement of the good-cube event, and the Gaussian shell estimate used by the successor site-tail construction.

1. The logarithmic weight of the moment bounds

theorem Algsuperdiff.Section5.Support.one_le_abs_log_gamma {d : ℕ} (M : Section3.ABKModel d) : 1 ≤ |Real.log M.gamma|

The scaling parameter is at most 1/4, so its logarithmic weight is at least log 4 > 1.

theorem Algsuperdiff.Section5.Support.abs_log_gamma_pos {d : ℕ} (M : Section3.ABKModel d) : 0 < |Real.log M.gamma|

2. The good-cube complement

theorem Algsuperdiff.Section5.Support.compl_goodCubeEvent_eq {d : ℕ} (M : Section3.ABKModel d) (Creg : ℝ) (n : ℤ) (y : HCPolySupport.Vec d) (ep : ℝ) : (goodCubeEvent M Creg n y ep)ᶜ = {omega : Section3.Cutoff.CutoffSample d | ENNReal.ofReal ep < localizedError M n y omega} ∪ {omega : Section3.Cutoff.CutoffSample d | ENNReal.ofReal (2 * Creg) < localizedRegularity M n y omega}

The good cube event fails exactly when one of the two localized quantities exceeds its threshold.

3. The shell estimate

theorem Algsuperdiff.Section5.Support.measureReal_shellExcessEvent_le {d : ℕ} (M : Section3.ABKModel d) {C0 ep : ℝ} (hC0 : 0 < C0) (hep : 0 < ep) (hgate : 1 ≤ C0 * ep * (√M.gamma)⁻¹) (n : ℤ) (L : ℕ) (z : Percolation.Site d) : (↑(Section3.Cutoff.cutoffSampleLaw M)).real (shellExcessEvent M C0 ep n L z) ≤ Real.exp (-(C0 ^ 2 * ep ^ 2 * M.gamma⁻¹ * 3 ^ (sitePathExponent * ↑L)))

The shell leg. The scale-L shell event has the Gaussian tail exp(-C_0² ε² γ^{-1} 3^{a L}) at the exponent a = 5/4, uniformly in the cube scale and the site: the normalization 3^{(2-γ) n} of the large-scale sum cancels the shell amplitude 3^{-n} 3^{(γ-1)(n+L)} exactly.