LargeScale

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

Large scales and the fixed-path weighted-cube bound

This file bounds the probability that an inflated cube of scale larger than the path length occurs on the path, and combines that with the small-scale bound into the fixed-path estimate for the weighted-cube event.

noncomputable def Algsuperdiff.Section5.Percolation.scaleOccurrenceEvent {Ω : Type u_1} {d : ℕ} (B : ℕ → Site d → Set Ω) (Γ : List (Site d)) (L : ℕ) : Set Ω

The event that an occurring inflated cube touches Γ at scale L.

Equations

• Algsuperdiff.Section5.Percolation.scaleOccurrenceEvent B Γ L = {ω : Ω | 0 < Algsuperdiff.Section5.Percolation.inflatedCubeCount B L Γ ω}

noncomputable def Algsuperdiff.Section5.Percolation.largeScaleOccurrenceEvent {Ω : Type u_1} {d : ℕ} (B : ℕ → Site d → Set Ω) (Γ : List (Site d)) : Set Ω

The union of occurring touched-cube events over scales larger than the path length.

Equations

• Algsuperdiff.Section5.Percolation.largeScaleOccurrenceEvent B Γ = ⋃ (L : ℕ), if Γ.length < 3 ^ L then Algsuperdiff.Section5.Percolation.scaleOccurrenceEvent B Γ L else ∅

theorem Algsuperdiff.Section5.Percolation.weightedCubeEvent_subset_largeScale_union_small {Ω : Type u_1} {d : ℕ} (B : ℕ → Site d → Set Ω) (Γ : List (Site d)) (r : ℝ) : weightedCubeEvent B Γ r ⊆ largeScaleOccurrenceEvent B Γ ∪ {ω : Ω | r < weightedCubeMassOn B Γ (smallScales Γ) ω}

A weighted partial sum can exceed a threshold only through a large-scale occurrence or through the canonical finite sum over small scales.

theorem Algsuperdiff.Section5.Percolation.measureReal_weightedCubeEvent_le_fixedPath {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (B : ℕ → Site d → Set Ω) (a T lam : ℝ) (hBmeas : ∀ (L : ℕ) (z : Site d), MeasurableSet (B L z)) (hsep : SepIndep P B) (hBtail : ∀ (L : ℕ) (z : Site d), P.real (B L z) ≤ Real.exp (-(T ^ 2 * 3 ^ (a * ↑L)))) (ha : 1 < a) (had : a ≤ ↑d) (hTone : 1 ≤ T) (hlam : 0 < lam) (hlamOne : lam < 1) (hgate : pathBoundGateConst d * lam⁻¹ * (a - 1)⁻¹ ≤ T) (Γ : List (Site d)) (hΓ : IsPath Γ) (hΓpos : 0 < Γ.length) : P.real (weightedCubeEvent B Γ (lam * ↑Γ.length / 2)) ≤ Real.exp (-(fixedPathRateConst d * ((a - 1) * T * lam) ^ 2 * ↑Γ.length))

A deterministic path obeys the weighted inflated-cube tail at the dimension-only rate used in the path union bound.