TranslatedCrossing

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

The crossing event at an arbitrary base site

The maximal-diameter bound measure_crossingEvent₂_le_exp (ABK26, l.percolation.bound.general, conclusion (3), e.diameter.bound) is stated for the origin-centred annulus □_{k+1} \ □_k. The consumers of that bound in Section 3.3 need it at an arbitrary base site w ∈ ℤ^d.

Nothing new is proved here: the abstract percolation layer is covariant under lattice translations, because latDist and cubeAt are. This module makes the covariance explicit by reindexing the family of bad events,

shiftFamily B w l y = B l (y + w).

The two hypotheses of measure_crossingEvent₂_le_exp — finite-range independence of the siteSigma σ-algebras and the uniform tail bound on the bad events — are transported to the reindexed family with no change of constants, since siteSigma (shiftFamily B w) S l = siteSigma B ((· + w) '' S) l and latDist (u + w) (v + w) = latDist u v.

Main definitions

• Algsuperdiff.Section3.Provider.Percolation.shiftFamily: the reindexed family of bad events.

Main results

• siteSigma_shiftFamily: the reindexing identity for the localised σ-algebras.
• indep_siteSigma_shiftFamily: finite-range independence transports to the reindexed family with the same range.
• measure_shiftFamily_le: a uniform tail bound transports to the reindexed family verbatim.

References

• ABK26, l.percolation.bound.general, e.diameter.bound.

Translation invariance of the lattice geometry

theorem Algsuperdiff.Section3.Provider.Percolation.latDist_add_right {d : ℕ} (x y w : Fin d → ℤ) : latDist (x + w) (y + w) = latDist x y

The sup distance is invariant under a common lattice translation.

theorem Algsuperdiff.Section3.Provider.Percolation.latDist_sub_right {d : ℕ} (x y w : Fin d → ℤ) : latDist (x - w) (y - w) = latDist x y

The sup distance is invariant under a common lattice translation, in subtracted form.

theorem Algsuperdiff.Section3.Provider.Percolation.latDist_zero_sub {d : ℕ} (z w : Fin d → ℤ) : latDist 0 (z - w) = latDist w z

The sup distance from the origin to a difference.

theorem Algsuperdiff.Section3.Provider.Percolation.mem_cubeAt_sub_zero {d k : ℕ} {z w : Fin d → ℤ} : z - w ∈ cubeAt k 0 ↔ z ∈ cubeAt k w

Recentring a triadic cube at the origin.

The reindexed family

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

The family of bad events reindexed by the lattice translation y ↦ y + w.

Equations

• Algsuperdiff.Section3.Provider.Percolation.shiftFamily B w l y = B l (y + w)

Transport of the two hypotheses

theorem Algsuperdiff.Section3.Provider.Percolation.siteSigma_shiftFamily {d : ℕ} {Ω : Type u_1} (B : ℕ → (Fin d → ℤ) → Set Ω) (w : Fin d → ℤ) (S : Set (Fin d → ℤ)) (k : ℕ) : siteSigma (shiftFamily B w) S k = siteSigma B ((fun (u : Fin d → ℤ) => u + w) '' S) k

The localised σ-algebras of the reindexed family are the localised σ-algebras of the original family at the translated set of sites.

theorem Algsuperdiff.Section3.Provider.Percolation.indep_siteSigma_shiftFamily {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {B : ℕ → (Fin d → ℤ) → Set Ω} (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) μ) (w : Fin d → ℤ) (l : ℕ) (S S' : Set (Fin d → ℤ)) (hsep : ∀ u ∈ S, ∀ v ∈ S', 3 ^ l < latDist u v) : ProbabilityTheory.Indep (siteSigma (shiftFamily B w) S l) (siteSigma (shiftFamily B w) S' l) μ

Finite-range independence transports to the reindexed family with the same range.

theorem Algsuperdiff.Section3.Provider.Percolation.measure_shiftFamily_le {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {B : ℕ → (Fin d → ℤ) → Set Ω} {c : ℕ → ENNReal} (hB : ∀ (L : ℕ) (y : Fin d → ℤ), μ (B L y) ≤ c L) (w : Fin d → ℤ) (L : ℕ) (y : Fin d → ℤ) : μ (shiftFamily B w L y) ≤ c L

A uniform tail bound transports to the reindexed family verbatim.

The diameter bound at an arbitrary base site