ClusterEventTwo

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

Distance-two cluster events and the scale-iteration inequality

LatticeTwo.lean supplied the geometry; this module transports the two probabilistic steps of Step 3 of the proof of l.percolation.bound.general to distance-two paths:

• measure_iInter_clusterEvent₂_le_pow — the factorisation of ABK26;
• measure_clusterEvent₂_add_le — the iteration inequality e.paths.ready.for.iteration of ABK26.

What changes against the proved distance-one layer

Nothing structural. The abstract σ-algebras siteSigma and the scale unions scaleUnion of ClusterEvent.lean are reused verbatim, so the finite-range independence hypothesis consumed here is literally the one the proved layer consumes (∀ u ∈ S, ∀ v ∈ S', 3 ^ l < latDist u v). Two numerical constants move, both by a dimension-only factor:

• the localisation boxes are locBox₂, one triadic generation wider than the distance-one boxes, so the union-bound weight is 3 ^ (d (k + h + 2)) instead of 3 ^ (d (k + h + 1)) — one extra 3 ^ d;
• the separation demanded of the extracted sites is 3 ^ (k+1) + 4 rather than 3 ^ (k+1) + 2.

The number 3 ^ (h - 3) of extracted sites, which is what the induction is driven by, is unchanged.

Main definitions

• clusterEvent₂: the event 𝒞_k(z) of ABK26 with distance-two paths.

Main results

• clusterEvent₂_eq_loc, measurableSet_clusterEvent₂: localisation.
• measure_iInter_clusterEvent₂_le_pow: ABK26.
• clusterEvent₂_subset_union, measure_clusterEvent₂_add_le: ABK26.

References

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

The distance-two cluster events

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

The event 𝒞_k(z) of ABK26, with the witnessing path allowed distance-two steps.

Equations

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

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

The localised form of 𝒞_k(z), in which the witnessing distance-two path is additionally required to stay inside locBox₂ k z.

Equations

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

theorem Algsuperdiff.Section3.Provider.Percolation.clusterEvent₂_eq_loc {d : ℕ} {Ω : Type u_1} (B : ℕ → (Fin d → ℤ) → Set Ω) (k : ℕ) (z : Fin d → ℤ) : clusterEvent₂ B k z = clusterEventLoc₂ B k z

Truncating a witnessing distance-two path at its first exit from z + □_k shows that the distance-two cluster event is localised.

theorem Algsuperdiff.Section3.Provider.Percolation.clusterEventLoc₂_eq_iUnion {d : ℕ} {Ω : Type u_1} (B : ℕ → (Fin d → ℤ) → Set Ω) (k : ℕ) (z : Fin d → ℤ) : clusterEventLoc₂ B k z = ⋃ (N : ℕ), ⋃ (x : Fin (N + 1) → Fin d → ℤ), ⋃ (_ : extendPath x 0 = z ∧ IsLatticePath₂ (extendPath x) N ∧ extendPath x N ∉ cubeAt k z ∧ ∀ (i : Fin (N + 1)), x i ∈ locBox₂ k z), ⋂ (i : Fin (N + 1)), scaleUnion B k (x i)

The localised distance-two cluster event as a countable union of finite intersections; the description used to establish measurability.

theorem Algsuperdiff.Section3.Provider.Percolation.measurableSet_clusterEvent₂ {d : ℕ} {Ω : Type u_1} (B : ℕ → (Fin d → ℤ) → Set Ω) (k : ℕ) (z : Fin d → ℤ) : MeasurableSet (clusterEvent₂ B k z)

The distance-two cluster event 𝒞_k(z) is measurable with respect to the σ-algebra of the bad events of scale at most k at the sites of locBox₂ k z. This is the localisation asserted at ABK26.

The product bound

theorem Algsuperdiff.Section3.Provider.Percolation.measure_iInter_clusterEvent₂_le_pow {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {B : ℕ → (Fin d → ℤ) → Set Ω} {k : ℕ} {p : ENNReal} (hindep : ∀ (S S' : Set (Fin d → ℤ)), (∀ u ∈ S, ∀ v ∈ S', 3 ^ k < latDist u v) → ProbabilityTheory.Indep (siteSigma B S k) (siteSigma B S' k) μ) (hp : ∀ (z : Fin d → ℤ), μ (clusterEvent₂ B k z) ≤ p) (M : ℕ) (y : ℕ → Fin d → ℤ) : (∀ (a b : ℕ), a < M → b < M → a ≠ b → 3 ^ (k + 1) + 4 ≤ latDist (y a) (y b)) → μ (⋂ m ∈ Set.Iio M, clusterEvent₂ B k (y m)) ≤ p ^ M

ABK26, for distance-two paths. If the finite-range independence hypothesis holds at range 3 ^ k — literally the hypothesis the proved distance-one layer consumes — and every distance-two cluster event has probability at most p, then for any M sites pairwise at sup distance at least 3 ^ (k + 1) + 4 the probability that all the corresponding cluster events occur is at most p ^ M.

The scale-iteration inequality

theorem Algsuperdiff.Section3.Provider.Percolation.clusterEvent₂_subset_union {d : ℕ} {Ω : Type u_1} {B : ℕ → (Fin d → ℤ) → Set Ω} {k h : ℕ} (hh : 3 ≤ h) (z : Fin d → ℤ) : clusterEvent₂ B (k + h) z ⊆ (⋃ y ∈ Fintype.piFinset fun (x : Fin (3 ^ (h - 3))) => locBox₂ (k + h) z, ⋃ (_ : ∀ (a b : Fin (3 ^ (h - 3))), a ≠ b → 3 ^ (k + 1) + 4 ≤ latDist (y a) (y b)), ⋂ m ∈ Set.Iio (3 ^ (h - 3)), clusterEvent₂ B k (tupleFun y m)) ∪ ⋃ z' ∈ locBox₂ (k + h) z, ⋃ l ∈ Finset.Icc (k + 1) (k + h), B l z'

The dichotomy of ABK26, for distance-two paths. If 𝒞_{k+h}(z) occurs then either there are 3 ^ (h - 3) sites in locBox₂ (k + h) z, pairwise at sup distance at least 3 ^ (k + 1) + 4, whose distance-two cluster events at scale k all occur, or some site of locBox₂ (k + h) z carries a bad event of a scale in [k + 1, k + h].

theorem Algsuperdiff.Section3.Provider.Percolation.measure_clusterEvent₂_add_le {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {B : ℕ → (Fin d → ℤ) → Set Ω} {k h : ℕ} {p q : ENNReal} (hh : 3 ≤ h) (hindep : ∀ (S S' : Set (Fin d → ℤ)), (∀ u ∈ S, ∀ v ∈ S', 3 ^ k < latDist u v) → ProbabilityTheory.Indep (siteSigma B S k) (siteSigma B S' k) μ) (hp : ∀ (w : Fin d → ℤ), μ (clusterEvent₂ B k w) ≤ p) (hq : ∀ (l : ℕ) (w : Fin d → ℤ), k + 1 ≤ l → l ≤ k + h → μ (B l w) ≤ q) (z : Fin d → ℤ) : μ (clusterEvent₂ B (k + h) z) ≤ (3 ^ (d * (k + h + 2)) * p) ^ 3 ^ (h - 3) + 3 ^ (d * (k + h + 2)) * ↑h * q

The iteration inequality e.paths.ready.for.iteration of ABK26, for distance-two paths.

If every distance-two cluster event at scale k has probability at most p, and every bad event B_l(z) with k < l ≤ k + h has probability at most q, then the distance-two cluster event at scale k + h has probability at most (W * p) ^ (3 ^ (h - 3)) + W * h * q with W = 3 ^ (d * (k + h + 2)). The distance-one layer has the same shape with W = 3 ^ (d * (k + h + 1)): the step size costs exactly one factor 3 ^ d.