PathBound

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

The multiscale percolation path bound

This file counts the crossing paths of a given vertex length, absorbs that count into the fixed-path exponent, and sums over lengths to obtain the path clause of the general percolation estimate.

noncomputable def Algsuperdiff.Section5.Percolation.fixedLengthWeightedPathEvent {Ω : Type u_1} {d : ℕ} (B : ℕ → Site d → Set Ω) (lam : ℝ) (k n : ℕ) : Set Ω

The event that a path of the prescribed length meets the weighted bad-cube threshold.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section5.Percolation.path_bound (d : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∃ (c : ℝ), 0 < c ∧ ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (B : ℕ → Site d → Set Ω) (a T lam : ℝ) (k : ℕ), (∀ (L : ℕ) (z : Site d), MeasurableSet (B L z)) → SepIndep P B → (∀ (L : ℕ) (z : Site d), P.real (B L z) ≤ Real.exp (-(T ^ 2 * 3 ^ (a * ↑L)))) → 1 < a → a ≤ ↑d → 1 ≤ T → 0 < lam → lam < 1 → C * lam⁻¹ * (a - 1)⁻¹ ≤ T → P.real {ω : Ω | ∃ (Γ : List (Site d)), IsPathFrom k Γ ∧ ∑ z ∈ Γ.toFinset, (badSet B z)ᶜ.indicator (fun (x : Ω) => 1) ω < (1 - lam) * 3 ^ k} ≤ Real.exp (-(c * (a - 1) ^ 2 * T ^ 2 * lam ^ 2 * 3 ^ k))

The path clause of the general percolation estimate, as stated in the pinned manuscript, lines 14222--14233. Only the path clause is formalized here; the density and maximal-diameter clauses are not asserted.

The source's independence across scales is not assumed: the path clause uses only the separation hypothesis, through the colouring of a single scale. ScaleIndep remains available for the density and maximal-diameter clauses.

The hypothesis a ≤ d is load-bearing. The scale summation ∑_L 3 ^ ((1 - a) * L / 2) ≤ C * (a - 1)⁻¹ behind the small-scale estimate is not uniform in a: the geometric tail factor (1 - 3 ^ (-(a - 1) / 2))⁻¹ tends to 1 as a grows, so no bound of that shape holds with a dimension-free constant. Under 1 < a ≤ d the factor is at most 2 * (d + 1) * (a - 1)⁻¹, which is the form used here.