ClusterEvent

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

The cluster events of ABK26 and their finite-range independence

This module introduces the events 𝒞_k(z) of ABK26, Step 3 of the proof of Lemma l.percolation.bound.general,

𝒞_k(z) := { there is a path Γ from {z} to ℤ^d \ (z + □_k) such that ⋂_{y ∈ Γ} (⋃_{L ∈ [0,k]} B_L(y)) occurs },

together with the two facts the proof uses about them:

• consequently, at pairwise sup distance at least 3 ^ (k + 1) + 2 the events 𝒞_k(y_i) factorise, which is the display at ABK26.

Formalisation of the independence hypothesis

ABK26, assumes: for each L ∈ ℕ and disjoint 𝒵, 𝒵' ⊆ ℤ^d with dist(𝒵,𝒵') > 3^L, the families {B_{L'}(z) : z ∈ 𝒵, L' ∈ [0,L]} and {B_{L'}(z) : z ∈ 𝒵', L' ∈ [0,L]} are independent. We render "the families are independent" as independence of the generated σ-algebras, siteSigma, which is Mathlib's ProbabilityTheory.Indep, and we render dist(𝒵,𝒵') > 3^L by the equivalent pointwise condition ∀ u ∈ 𝒵, ∀ v ∈ 𝒵', 3^L < latDist u v (on a lattice with an ℕ-valued metric the infimum over a nonempty pair of sets is attained, so the two readings agree; the pointwise form also covers the degenerate empty cases). Disjointness of 𝒵 and 𝒵' is implied by the distance condition.

Main definitions

• Algsuperdiff.Section3.Provider.Percolation.scaleUnion: the event ⋃_{L ∈ [0,k]} B_L(y).
• Algsuperdiff.Section3.Provider.Percolation.extendPath: a finite tuple of sites read as a function on ℕ, by repeating its last entry.
• Algsuperdiff.Section3.Provider.Percolation.siteSigma: the σ-algebra generated by the bad events of scale at most k at the sites of a given set.

Main results

• mem_scaleUnion_iff, extendPath_apply: the pointwise characterisations of scaleUnion and of extendPath.
• siteSigma_mono: the localised σ-algebras grow with the site set.
• measurableSet_scaleUnion: at a site of S, the scale-k union is siteSigma B S k-measurable.

References

• ABK26, proof of l.percolation.bound.general, Step 3.

The events

def Algsuperdiff.Section3.Provider.Percolation.scaleUnion {d : ℕ} {Ω : Type u_1} (B : ℕ → (Fin d → ℤ) → Set Ω) (k : ℕ) (y : Fin d → ℤ) : Set Ω

⋃_{L ∈ [0,k]} B_L(y): some bad event of scale at most k occurs at y.

Equations

• Algsuperdiff.Section3.Provider.Percolation.scaleUnion B k y = ⋃ L ∈ Set.Iic k, B L y

theorem Algsuperdiff.Section3.Provider.Percolation.mem_scaleUnion_iff {d : ℕ} {Ω : Type u_1} {B : ℕ → (Fin d → ℤ) → Set Ω} {k : ℕ} {y : Fin d → ℤ} {ω : Ω} : ω ∈ scaleUnion B k y ↔ ∃ L ≤ k, ω ∈ B L y

A countable description

def Algsuperdiff.Section3.Provider.Percolation.extendPath {d N : ℕ} (x : Fin (N + 1) → Fin d → ℤ) : ℕ → Fin d → ℤ

Extend a tuple of sites indexed by Fin (N + 1) to a function on ℕ by repeating the last entry.

Equations

• Algsuperdiff.Section3.Provider.Percolation.extendPath x i = x ⟨min i N, ⋯⟩

theorem Algsuperdiff.Section3.Provider.Percolation.extendPath_apply {d N : ℕ} (x : Fin (N + 1) → Fin d → ℤ) {i : ℕ} (hi : i ≤ N) : extendPath x i = x ⟨i, ⋯⟩

The localised σ-algebras

@[reducible, inline]

abbrev Algsuperdiff.Section3.Provider.Percolation.siteSigma {d : ℕ} {Ω : Type u_1} (B : ℕ → (Fin d → ℤ) → Set Ω) (S : Set (Fin d → ℤ)) (k : ℕ) : MeasurableSpace Ω

The σ-algebra generated by the bad events of scale at most k at the sites of S; this is the σ-algebra of the family {B_{L'}(z) : z ∈ S, L' ∈ [0,k]} of ABK26.

Equations

• Algsuperdiff.Section3.Provider.Percolation.siteSigma B S k = MeasurableSpace.generateFrom {A : Set Ω | ∃ L ≤ k, ∃ y ∈ S, A = B L y}

theorem Algsuperdiff.Section3.Provider.Percolation.siteSigma_mono {d : ℕ} {Ω : Type u_1} (B : ℕ → (Fin d → ℤ) → Set Ω) {S S' : Set (Fin d → ℤ)} (hS : S ⊆ S') (k : ℕ) : siteSigma B S k ≤ siteSigma B S' k

theorem Algsuperdiff.Section3.Provider.Percolation.measurableSet_scaleUnion {d : ℕ} {Ω : Type u_1} {B : ℕ → (Fin d → ℤ) → Set Ω} {S : Set (Fin d → ℤ)} {k : ℕ} {y : Fin d → ℤ} (hy : y ∈ S) : MeasurableSet (scaleUnion B k y)

The product bound