SiteFamilyBridge

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

The site family of l.percolation.bad.clusters and its independence

This module proves a local finite-range result used by l.percolation.bad.clusters (ABK26): it turns the abstract percolation layer's independence hypothesis

∀ l S S', (∀ u ∈ S, ∀ v ∈ S', 3 ^ l < latDist u v) →
  Indep (siteSigma B S l) (siteSigma B S' l) mu

into a theorem for an explicit implementation B of the manuscript's scale-L bad events, with no independence assumed anywhere: everything is routed through the proved cutoff range lemma, which is itself routed through the frozen (J1) unit-range-dependence assumption.

The three disclosed constants

1. Region radius (sharp). cubeTreeRegion Q — the union of the closed cubes of the nine-generation descendant tree of Q — is exactly the closed sup-ball Metric.closedBall (cubeBasePoint Q) ((1/2) * 3 ^ Q.scale), i.e. the closed cube itself (cubeTreeRegion_subset_closedBall_half). The concentric double of SiteFamily.cubeTreeRegion_subset_closedBall is not optimal: a descendant R ⊆ Q has its closed cube inside the closed cube of Q, so the constant 1 is replaced by the sharp 1/2 here.

2. Lattice-to-Euclidean conversion. Two sites u, v of the base lattice 3^base Z^d at sup-lattice distance latDist u v carry tree regions whose Euclidean distance is at least (latDist u v - 1) * 3 ^ base (vecNorm_sub_ge_of_mem_cubeTreeRegion). The - 1 is the sharp radius of item 1 counted twice (1/2 + 1/2).

3. The reindexing shift (the manuscript's "after reindexing"). The level-L bad event of a base-scale cube reads shells of index at most `base

   • L; the proved cutoff range lemma indep_cutoffShellLocalSigma_of_separationtherefore needs the *Euclidean* separationsqrt(d) * 3 ^ (base + L), i.e. lattice separation 1 + sqrt(d)
   • 3 ^ L, whereas the abstract layer supplies only 3 ^ L < latDist. The sqrt(d)is intrinsic: it is the literal hypothesis of the frozen (J1) assumption (a unit cube has Euclidean diametersqrt(d)), and it cannot be removed downstream. The manuscript's own sentence "satisfy (after reindexing) the independence requirements of Lemma~\ref{l.percolation.bound.general}" is implemented locally by the explicit shift sepShift d = d, which satisfies sqrt(d) <= 3 ^ (sepShift d)`:

   siteBadEvent M base l u = if l < sepShift d then ∅
                             else badScaleEvent M (siteCube base u) (l - sepShift d)
   

   The shift costs exactly a factor 3 ^ (-a * sepShift d) in the tail parameter T ^ 2 (a d-dependent constant, which is what the manuscript's C(d) absorbs) and nothing else: the union ⋃ l, siteBadEvent M base l u is unchanged, because l ↦ l - sepShift d is onto N on l ≥ sepShift d.

Main results

• cubeTreeRegion_subset_closedBall_half: the sharp region radius.
• measurableSet_badScaleEvent_zero_cutoffSampleLocal: locality of level 0 of the D-9 family (the badLoc level), completing measurableSet_badScaleEvent_succ_cutoffShellLocal.
• measurableSet_badScaleEvent_cutoffSampleLocal: locality of every level.
• siteSigma_le_cutoffSampleLocalSigma: the siteSigma bridge.
• indep_siteSigma_siteBadEvent: the abstract layer's hindep, discharged.

References

• ABK26, l.percolation.bad.clusters.
• ABK26, l.percolation.bound.general.

The sharp radius of the descendant-tree region

theorem Algsuperdiff.Section3.Provider.Percolation.closedBall_subset_closedBall_of_cubeSet_subset {d : ℕ} {Q R : HCPolySupport.TriadicCube d} (h : HCPolySupport.cubeSet R ⊆ HCPolySupport.cubeSet Q) : Metric.closedBall (BadEvents.cubeBasePoint R) (1 / 2 * 3 ^ R.scale) ⊆ Metric.closedBall (BadEvents.cubeBasePoint Q) (1 / 2 * 3 ^ Q.scale)

A subcube's closed cube lies in the ambient closed cube. This is the sharp form of the concentric bound: the closed sup-ball of radius (1/2) 3 ^ R.scale around cubeBasePoint R is the closed cube R, and the closed cubes of the descendants of Q are contained in the closed cube Q.

theorem Algsuperdiff.Section3.Provider.Percolation.cubeTreeRegion_subset_closedBall_half {d : ℕ} (Q : HCPolySupport.TriadicCube d) : cubeTreeRegion Q ⊆ Metric.closedBall (BadEvents.cubeBasePoint Q) (1 / 2 * 3 ^ Q.scale)

The sharp disclosed range constant. The nine-generation descendant tree of Q lives in the closed sup-ball of radius (1/2) 3 ^ Q.scale around the base point, i.e. in the closed cube Q itself.

theorem Algsuperdiff.Section3.Provider.Percolation.cubeSet_subset_cubeTreeRegion_of_mem_descendantsAtScale {d : ℕ} {Q R : HCPolySupport.TriadicCube d} {i : ℕ} (hi : i ∈ Finset.range 10) (hR : R ∈ HCPolySupport.descendantsAtScale Q (Q.scale - ↑i)) : HCPolySupport.cubeSet R ⊆ cubeTreeRegion Q

The closed cube of a descendant of Q is inside the tree region of Q.

theorem Algsuperdiff.Section3.Provider.Percolation.measurableSet_cubeTreeRegion {d : ℕ} (Q : HCPolySupport.TriadicCube d) : MeasurableSet (cubeTreeRegion Q)

Locality of every level of the site family

theorem Algsuperdiff.Section3.Provider.Percolation.measurableSet_badScaleEvent_zero_cutoffSampleLocal {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) {U : Set (HCPolySupport.Vec d)} (hU : cubeTreeRegion Q ⊆ U) : MeasurableSet (badScaleEvent M Q 0)

Level 0 of the D-9 family is integral-local. Together with the proved measurableSet_badScaleEvent_succ_cutoffShellLocal this proves the local Provider result for the locality part of l.percolation.bound.general for the manuscript's scale-resolved bad events.

theorem Algsuperdiff.Section3.Provider.Percolation.measurableSet_badScaleEvent_cutoffSampleLocal {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (l : ℕ) {U : Set (HCPolySupport.Vec d)} (hU : cubeTreeRegion Q ⊆ U) : MeasurableSet (badScaleEvent M Q l)

Locality of every level of the D-9 family, in the completed cutoff-sample local sigma-field at the exact shell index Q.scale + l.

The site family of e.bad.cluster.def

def Algsuperdiff.Section3.Provider.Percolation.siteCube {d : ℕ} (base : ℤ) (u : Fin d → ℤ) : HCPolySupport.TriadicCube d

The base-scale triadic cube z + square_base at the lattice site u, i.e. z = 3^base u.

Equations

• Algsuperdiff.Section3.Provider.Percolation.siteCube base u = { scale := base, index := u }

@[simp]

theorem Algsuperdiff.Section3.Provider.Percolation.siteCube_scale {d : ℕ} (base : ℤ) (u : Fin d → ℤ) : (siteCube base u).scale = base

def Algsuperdiff.Section3.Provider.Percolation.sepShift (d : ℕ) : ℕ

The disclosed reindexing shift. Any q with sqrt(d) ≤ 3 ^ q works; q = d is the explicit choice made here.

Equations

• Algsuperdiff.Section3.Provider.Percolation.sepShift d = d

theorem Algsuperdiff.Section3.Provider.Percolation.sqrt_le_three_pow_sepShift (d : ℕ) : √↑d ≤ 3 ^ sepShift d

def Algsuperdiff.Section3.Provider.Percolation.siteBadEvent {d : ℕ} (M : ABKModel d) (base : ℤ) (l : ℕ) (u : Fin d → ℤ) : Set (Cutoff.CutoffSample d)

The reindexed scale-l bad event of l.percolation.bad.clusters. The levels below the disclosed shift are empty; from the shift on, this is exactly the manuscript's B_L(z + cu_base) with L = l - sepShift d.

Equations

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

theorem Algsuperdiff.Section3.Provider.Percolation.measurableSet_siteBadEvent {d : ℕ} (M : ABKModel d) (base : ℤ) (l : ℕ) (u : Fin d → ℤ) : MeasurableSet (siteBadEvent M base l u)

theorem Algsuperdiff.Section3.Provider.Percolation.badExtended_subset_iUnion_siteBadEvent {d : ℕ} (M : ABKModel d) (base : ℤ) (u : Fin d → ℤ) : BadEvents.badExtended M (siteCube base u) ⊆ ⋃ (l : ℕ), siteBadEvent M base l u

The reindexing loses nothing: the union over the reindexed levels is the union over the manuscript's own levels, so the manuscript's inclusion B^*(z + cu_base) ⊆ ⋃_L B_L(z + cu_base) survives verbatim.

The observation region of a set of sites

def Algsuperdiff.Section3.Provider.Percolation.siteRegion {d : ℕ} (base : ℤ) (S : Set (Fin d → ℤ)) : Set (HCPolySupport.Vec d)

The spatial region read by the whole site family at the sites of S.

Equations

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

theorem Algsuperdiff.Section3.Provider.Percolation.measurableSet_siteRegion {d : ℕ} (base : ℤ) (S : Set (Fin d → ℤ)) : MeasurableSet (siteRegion base S)

theorem Algsuperdiff.Section3.Provider.Percolation.cubeTreeRegion_subset_siteRegion {d : ℕ} {base : ℤ} {S : Set (Fin d → ℤ)} {u : Fin d → ℤ} (hu : u ∈ S) : cubeTreeRegion (siteCube base u) ⊆ siteRegion base S

The lattice-to-Euclidean separation conversion

theorem Algsuperdiff.Section3.Provider.Percolation.vecNorm_sub_ge_of_mem_cubeTreeRegion {d : ℕ} (hd : 0 < d) (base : ℤ) {u v : Fin d → ℤ} {x y : HCPolySupport.Vec d} (hx : x ∈ cubeTreeRegion (siteCube base u)) (hy : y ∈ cubeTreeRegion (siteCube base v)) : (↑(latDist u v) - 1) * 3 ^ base ≤ HCPolySupport.Book.Ch02.vecNorm (x - y)

The disclosed separation conversion. Two base-scale sites at sup lattice distance latDist u v have descendant-tree regions at Euclidean distance at least (latDist u v - 1) * 3 ^ base. The - 1 is the sharp region radius 1/2 counted at both sites.

The siteSigma bridge and the independence discharge

theorem Algsuperdiff.Section3.Provider.Percolation.siteSigma_le_cutoffSampleLocalSigma {d : ℕ} (M : ABKModel d) (base : ℤ) (l : ℕ) (S : Set (Fin d → ℤ)) : siteSigma (siteBadEvent M base) S l ≤ Cutoff.cutoffSampleLocalSigma M (base + ↑(l - sepShift d)) (siteRegion base S)

The siteSigma bridge. All the information the site family at the sites of S carries up to level l is integral-local information of the shells of index at most base + (l - sepShift d) in the region siteRegion.

theorem Algsuperdiff.Section3.Provider.Percolation.indep_siteSigma_siteBadEvent {d : ℕ} (M : ABKModel d) (base : ℤ) (l : ℕ) (S S' : Set (Fin d → ℤ)) (hsep : ∀ u ∈ S, ∀ v ∈ S', 3 ^ l < latDist u v) : ProbabilityTheory.Indep (siteSigma (siteBadEvent M base) S l) (siteSigma (siteBadEvent M base) S' l) ↑(Cutoff.cutoffSampleLaw M)

The independence hypothesis of l.percolation.bound.general, discharged. Nothing is assumed: the two site families at sup-lattice separation more than 3 ^ l generate integral-local information on two regions whose Euclidean separation exceeds the literal cutoff range sqrt(d) * 3 ^ (base + l - sepShift d), and the proved cutoff range lemma — routed through the frozen (J1) unit-range assumption — supplies the independence.