DiameterTwo

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

The maximal diameter bound for distance-two crossings

It proves a local scale-induction result e.Ck.indy.hyp and the final union bound for distance-two paths, delivering conclusion (3) of l.percolation.bound.general — the maximal diameter bound e.diameter.bound — for the crossing event whose paths step by two.

The gate constant does not grow

The distance-two layer is proved under exactly the threshold of the distance-one layer,

16 d exp(40 (1 - b)^{-1}) ≤ T² b

The reason the constant survives is arithmetic, and is worth recording. The step size enters the induction only through

• the union-bound weight 3 ^ (d (k + h + 2)) instead of 3 ^ (d (k + h + 1)) (one extra 3 ^ d from the wider localisation box locBox₂), and
• the corresponding 3 ^ (d (k + 2)), 3 ^ (d (k + 3)) in the final union bound,

whereas the number 3 ^ (h - 3) of separated sites extracted from a long path is unchanged (LatticeTwo.exists_separated_subpaths₂). In the scalar inequalities this replaces the hypothesis h + 1 ≤ 3 ^ h by h + 2 ≤ 3 ^ h and the entropy d (j + h + 1) by d (j + h + 2), both of which are absorbed by the slack already present at 3 ^ h ≥ 27. No constant in the gate or in the conclusion moves.

Main definitions

• crossingEvent₂, crossingEvent₂At: the crossing event of e.diameter.bound with distance-two paths, at the origin and at an arbitrary base site.

Main results

• measure_clusterEvent₂_le_exp: the induction e.Ck.indy.hyp.
• measure_crossingEvent₂_le_exp: e.diameter.bound for distance-two crossings.
• measure_crossingEvent₂At_le_exp: the same at an arbitrary base site.

References

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

An elementary count

The scalar inequalities driving the induction

The base case

The induction

theorem Algsuperdiff.Section3.Provider.Percolation.measure_clusterEvent₂_le_exp {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {B : ℕ → (Fin d → ℤ) → Set Ω} {a b T : ℝ} {h : ℕ} (hd : 1 ≤ d) (hh : 3 ≤ h) (hb0 : 0 < b) (hb1 : b ≤ 1) (hba : b ≤ a) (hgain : 8 ≤ (1 - b) * ↑h) (hT : 16 * ↑d * 9 ^ h ≤ T ^ 2 * b) (hindep : ∀ (l : ℕ) (S S' : Set (Fin d → ℤ)), (∀ u ∈ S, ∀ v ∈ S', 3 ^ l < latDist u v) → ProbabilityTheory.Indep (siteSigma B S l) (siteSigma B S' l) μ) (hB : ∀ (L : ℕ) (w : Fin d → ℤ), μ (B L w) ≤ ENNReal.ofReal (Real.exp (-(T ^ 2 * 3 ^ (a * ↑L))))) (k : ℕ) (z : Fin d → ℤ) : μ (clusterEvent₂ B k z) ≤ ENNReal.ofReal (Real.exp (-(T ^ 2 * 3 ^ (b * (↑k - ↑h)) / 2)))

The induction e.Ck.indy.hyp of ABK26, for distance-two paths.

Under the finite-range independence hypothesis of l.percolation.bound.general — literally the hypothesis the proved distance-one layer consumes — and the tail bound e.badevent.upperbound.appendix, every distance-two cluster event obeys μ(𝒞_k(z)) ≤ exp(-½ T² 3^{b(k-h)}).

The hypotheses, including the threshold 16 d 9^h ≤ T² b, are identical to the distance-one measure_clusterEvent_le_exp.

The distance-two crossing event

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

The event of ABK26 e.diameter.bound with distance-two paths: some distance-two lattice path from ℤ^d ∩ □_k to ℤ^d \ □_{k+1} has B(z) = ⋃_L B_L(z) occurring at each site.

Equations

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

theorem Algsuperdiff.Section3.Provider.Percolation.crossingEvent₂_subset {d : ℕ} {Ω : Type u_1} (B : ℕ → (Fin d → ℤ) → Set Ω) (k : ℕ) : crossingEvent₂ B k ⊆ (⋃ z ∈ locBox₂ k 0, clusterEvent₂ B k z) ∪ ⋃ z' ∈ locBox₂ (k + 1) 0, ⋃ (j : ℕ), ⋃ (_ : k < j), B j z'

The union bound of ABK26, for distance-two paths.

The geometric tail over the large scales

The scalar inequalities of the final union bound

The distance-two diameter bound

theorem Algsuperdiff.Section3.Provider.Percolation.measure_crossingEvent₂_le_exp_of_scale {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {B : ℕ → (Fin d → ℤ) → Set Ω} {a b T γ : ℝ} {h : ℕ} (hd : 1 ≤ d) (hh : 3 ≤ h) (hb0 : 0 < b) (hb1 : b ≤ 1) (hba : b ≤ a) (hgain : 8 ≤ (1 - b) * ↑h) (hT : 16 * ↑d * 9 ^ h ≤ T ^ 2 * b) (hindep : ∀ (l : ℕ) (S S' : Set (Fin d → ℤ)), (∀ u ∈ S, ∀ v ∈ S', 3 ^ l < latDist u v) → ProbabilityTheory.Indep (siteSigma B S l) (siteSigma B S' l) μ) (hB : ∀ (L : ℕ) (w : Fin d → ℤ), μ (B L w) ≤ ENNReal.ofReal (Real.exp (-(T ^ 2 * 3 ^ (a * ↑L))))) (k : ℕ) (hγ0 : 0 ≤ γ) (hγ : 8 * 3 ^ h * γ ≤ T ^ 2 * 3 ^ (b * ↑k)) : μ (crossingEvent₂ B k) ≤ ENNReal.ofReal (Real.exp (-γ))

The maximal diameter bound for distance-two crossings, with the scale h and the target exponent γ left explicit.

theorem Algsuperdiff.Section3.Provider.Percolation.measure_crossingEvent₂_le_exp {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {B : ℕ → (Fin d → ℤ) → Set Ω} {a b T : ℝ} (hd : 1 ≤ d) (hb0 : 0 < b) (hb1 : b < 1) (hba : b ≤ a) (hT : 16 * ↑d * Real.exp (40 / (1 - b)) ≤ T ^ 2 * b) (hindep : ∀ (l : ℕ) (S S' : Set (Fin d → ℤ)), (∀ u ∈ S, ∀ v ∈ S', 3 ^ l < latDist u v) → ProbabilityTheory.Indep (siteSigma B S l) (siteSigma B S' l) μ) (hB : ∀ (L : ℕ) (w : Fin d → ℤ), μ (B L w) ≤ ENNReal.ofReal (Real.exp (-(T ^ 2 * 3 ^ (a * ↑L))))) (k : ℕ) : μ (crossingEvent₂ B k) ≤ ENNReal.ofReal (Real.exp (-(Real.exp (-(40 / (1 - b))) * T ^ 2 * 3 ^ (b * ↑k) / 2)))

ABK26, l.percolation.bound.general, conclusion (3), e.diameter.bound, for distance-two crossings.

Hypotheses and constants are identical to the proved distance-one measure_crossingEvent_le_exp: the threshold 16 d exp(40 (1-b)^{-1}) ≤ T² b and the conclusion exp(-½ exp(-40 (1-b)^{-1}) T² 3^{bk}) with the same explicit C = 40.

The distance-two crossing event at an arbitrary base site

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

The crossing event of ABK26 e.diameter.bound at an arbitrary base site w, with distance-two paths.

Equations

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

theorem Algsuperdiff.Section3.Provider.Percolation.crossingEvent₂At_eq_crossingEvent₂_shiftFamily {d : ℕ} {Ω : Type u_1} (B : ℕ → (Fin d → ℤ) → Set Ω) (k : ℕ) (w : Fin d → ℤ) : crossingEvent₂At B k w = crossingEvent₂ (shiftFamily B w) k

The reindexing identity. The distance-two crossing event of B at base site w is the origin-centred distance-two crossing event of the reindexed family shiftFamily B w.

theorem Algsuperdiff.Section3.Provider.Percolation.measure_crossingEvent₂At_le_exp {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {B : ℕ → (Fin d → ℤ) → Set Ω} {a b T : ℝ} (hd : 1 ≤ d) (hb0 : 0 < b) (hb1 : b < 1) (hba : b ≤ a) (hT : 16 * ↑d * Real.exp (40 / (1 - b)) ≤ T ^ 2 * b) (hindep : ∀ (l : ℕ) (S S' : Set (Fin d → ℤ)), (∀ u ∈ S, ∀ v ∈ S', 3 ^ l < latDist u v) → ProbabilityTheory.Indep (siteSigma B S l) (siteSigma B S' l) μ) (hB : ∀ (L : ℕ) (w : Fin d → ℤ), μ (B L w) ≤ ENNReal.ofReal (Real.exp (-(T ^ 2 * 3 ^ (a * ↑L))))) (k : ℕ) (w : Fin d → ℤ) : μ (crossingEvent₂At B k w) ≤ ENNReal.ofReal (Real.exp (-(Real.exp (-(40 / (1 - b))) * T ^ 2 * 3 ^ (b * ↑k) / 2)))

ABK26, e.diameter.bound, for distance-two crossings at an arbitrary base site. Identical hypotheses and identical constants as measure_crossingEvent₂_le_exp; only the centre of the annulus moves.