PercolationAssemblyV2

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

Chains of good cubes at the successor logarithmic exponents

This module reruns the lattice-path assembly with the successor per-site tail. The localized-error moment input is supplied internally, while the successor localized-regularity moment estimate remains one explicit hypothesis. A second theorem supplies that estimate from the Section 4 statement and so states the assembly with no hypothesis beyond the model.

noncomputable def Algsuperdiff.Section5.Provider.siteShiftedTailConstV2 (d : ℕ) (c : ℝ) : ℝ

The tail constant after the site-path separation shift.

Equations

• Algsuperdiff.Section5.Provider.siteShiftedTailConstV2 d c = c / 2 * 3 ^ (-(Algsuperdiff.Section5.Support.sitePathExponent * ↑(Algsuperdiff.Section3.Provider.Percolation.sepShift d)))

theorem Algsuperdiff.Section5.Provider.percolation_GF_v2_provider_of_hmomX (d : ℕ) (cstar : ℝ) (hcstar : 0 < cstar) (Cinj : ℝ) (hCinj : 0 < Cinj) (hmomX : ∃ (gamma0 : ℝ) (creg : ℝ) (Creg : ℝ), 0 < gamma0 ∧ 0 < creg ∧ 0 < Creg ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ gamma0 → ∀ (n : ℤ) (y : HCPolySupport.Vec d), ∫⁻ (omega : Section3.Cutoff.CutoffSample d), Support.localizedRegularity M n y omega ^ (creg * M.gamma⁻¹ * |Real.log M.gamma| ^ (-6)) ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal Creg ^ (creg * M.gamma⁻¹ * |Real.log M.gamma| ^ (-6))) : ∃ (gamma0 : ℝ) (c : ℝ) (C : ℝ) (Creg : ℝ), 0 < gamma0 ∧ 0 < c ∧ 0 < C ∧ 0 < Creg ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ gamma0 → ∀ ep ∈ Set.Icc (C * √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 * 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 ≤ ↑(Support.qSiteCount M Creg Cinj n ep (Percolation.pathSites N x) omega)

The successor chains-of-good-cubes estimate, conditional only on the successor localized-regularity moment bound.

theorem Algsuperdiff.Section5.Provider.percolation_GF_v2_provider (d : ℕ) (cstar : ℝ) (hcstar : 0 < cstar) (Cinj : ℝ) (hCinj : 0 < Cinj) : ∃ (gamma0 : ℝ) (c : ℝ) (C : ℝ) (Creg : ℝ), 0 < gamma0 ∧ 0 < c ∧ 0 < C ∧ 0 < Creg ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ gamma0 → ∀ ep ∈ Set.Icc (C * √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 * 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 ≤ ↑(Support.qSiteCount M Creg Cinj n ep (Percolation.pathSites N x) omega)

The successor chains-of-good-cubes estimate, with the successor localized-regularity moment bound supplied.