PercolationScaleV2

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

The percolation scale from the successor estimate

The successor chains-of-good-cubes estimate is stated with injection constant 1. This module transports its crossing count to an arbitrary positive injection constant by the accuracy rescaling of the joint event. The resulting supplier has the successor logarithmic floor and tail exponent.

theorem Algsuperdiff.Section5.Support.exists_measurable_scale_ae_crossing_v2 (d : ℕ) (cstar : ℝ) (hcstar : 0 < cstar) : ∃ (gamma0 : ℝ) (c : ℝ) (C : ℝ) (Creg : ℝ), 0 < gamma0 ∧ 0 < c ∧ 0 < C ∧ 0 < Creg ∧ ∀ (Cinj : ℝ), 0 < Cinj → ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ gamma0 → ∀ ep ∈ Set.Icc (C * max 1 Cinj * √M.gamma * |Real.log M.gamma|.rpow (7 / 2)) (1 / 4), ∀ (m : ℤ), ∃ (Y : Section3.Cutoff.CutoffSample d → ℕ), Measurable Y ∧ (∀ (N : ℕ), 1 ≤ N → ↑(Section3.Cutoff.cutoffSampleLaw M) {omega : Section3.Cutoff.CutoffSample d | N ≤ Y omega} ≤ ENNReal.ofReal (Real.exp (-(c / max 1 Cinj ^ 2 * ep ^ 2 * M.gamma⁻¹ * |Real.log M.gamma| ^ (-6) * 3 ^ N)))) ∧ ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), ∀ n ≤ m - ↑(Y omega), ∀ (N : ℕ) (x : ℕ → Fin d → ℤ), Section3.Provider.Percolation.IsLatticePath x N → x 0 ∈ Section3.Provider.Percolation.cubeAt (m - n).toNat 0 → x N ∉ Section3.Provider.Percolation.cubeAt ((m - n).toNat + 1) 0 → 3 / 4 * 3 ^ (m - n).toNat ≤ ↑(qSiteCount M Creg Cinj n ep (Percolation.pathSites N x) omega)

The successor percolation estimate, transported from injection constant 1 to an arbitrary positive injection constant. Rescaling by K = max 1 Cinj weakens the anchor's accuracy floor by the factor K and its exponential rate by the factor K ^ 2.