Hypotheses

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

Probabilistic hypotheses for multiscale percolation

This file records the scale-independence and spatial-separation hypotheses, the union of bad events over scales, and the measurable crossing-path event.

def Algsuperdiff.Section5.Percolation.SepIndep {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (P : MeasureTheory.Measure Ω) (B : ℕ → Site d → Set Ω) : Prop

Mutual independence of spatial-block sigma-algebras at scales at most L, for any finite family of blocks separated by more than 3^L in the lattice sup distance.

The source states the two-block form SepTwoBlockIndep, which implies this mutual form by sepIndep_of_twoBlock. Sites inside one block need not be separated, which is essential when an inflated event is generated by every site of a cube.

Equations

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

def Algsuperdiff.Section5.Percolation.SepTwoBlockIndep {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (P : MeasureTheory.Measure Ω) (B : ℕ → Site d → Set Ω) : Prop

The source's two-block separation hypothesis: for any scale L and any two sets of sites at lattice sup distance more than 3^L, the sigma-algebras generated by the events of scale at most L over those sites are independent (pinned manuscript, line 14196). Separation already forces the two sets to be disjoint, so disjointness is not assumed separately.

Equations

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

theorem Algsuperdiff.Section5.Percolation.sepIndep_of_twoBlock {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] {B : ℕ → Site d → Set Ω} (h : SepTwoBlockIndep P B) : SepIndep P B

The two-block separation hypothesis of the source implies mutual independence of the spatial blocks of a separated finite family.

def Algsuperdiff.Section5.Percolation.badSet {Ω : Type u_1} {d : ℕ} (B : ℕ → Site d → Set Ω) (z : Site d) : Set Ω

The bad event at a site, obtained by taking the union over all scales.

Equations

• Algsuperdiff.Section5.Percolation.badSet B z = ⋃ (L : ℕ), B L z

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

The number of distinct good vertices of a path, represented as a real random variable. Passing through toFinset implements the vertex-set reading when a path repeats a site.

Equations

• Algsuperdiff.Section5.Percolation.goodVertexCount B Γ ω = ∑ z ∈ Γ.toFinset, (Algsuperdiff.Section5.Percolation.badSet B z)ᶜ.indicator (fun (x : Ω) => 1) ω

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

The event that some crossing path has fewer than the prescribed number of good vertices.

Equations

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