SiteFamily

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

The scale-resolved bad-event family of l.percolation.bad.clusters

The aggregate extended bad event B^*(z + square_j) is not finite range at any fixed range: its oscillation part B_osc is a union over all shells L > j, and the shell j_L has range 3^L. The manuscript therefore never feeds B^* itself into the abstract percolation lemma l.percolation.bound.general (ABK26); it feeds a two-indexed family, the scale-L bad events of the proof of l.percolation.bad.clusters (ABK26):

B_0(z + cu_{m-h})   = ⋃_{i=0}^{9} ⋃_{z'} B_loc(z' + cu_{m-h-i})
B_L(z + cu_{m-h})   = ⋃_{i=0}^{9} ⋃_{z'} B_{osc, m-h-i+L}(z' + cu_{m-h-i})   (L ≥ 1)

with B^*(z + cu_{m-h}) ⊆ ⋃_{L ∈ N_0} B_L(z + cu_{m-h}).

This module defines that family as badScaleEvent, proves the manuscript's inclusion, and proves the locality half of the independence requirement of l.percolation.bound.general for every positive level: the level-l event of a cube of scale j is measurable for the integral-local sigma-field of the shells of index at most j + l on a ball of radius 3^j around the cube's base point. Independence at the matching separation is then the proved cutoff range lemma.

Range constants (disclosed)

• cubeTreeRegion Q — the union of the closed cubes of the nine-generation descendant tree of Q — is contained in Metric.closedBall (cubeBasePoint Q) (3 ^ Q.scale), i.e. in the closed sup-ball of radius 3^j (twice the closed cube z + \bar{square}_j). The factor 2 is the crude bound dist(z', z) + 3^{j-i}/2 ≤ 3^j/2 + 3^j/2; it is not optimized.
• badScaleEvent M Q (l+1) reads only shells of index ≤ Q.scale + l + 1.
• Consequently two cubes whose 3^{Q.scale}-balls are separated by √d · 3^{Q.scale + l + 1} in the Euclidean norm carry independent level-≤ l+1 information. The √d is the ℓ∞-to-Euclidean conversion already built into indep_lowerShellLocalSigma_of_cutoff_separation; it is the literal hypothesis shape of the proved lemma and is not weakened here.

Main definitions

• cubeTreeRegion: the spatial region read by the whole descendant tree.
• badScaleEvent: the manuscript's B_L(z + cu_{m-h}).
• cutoffShellLocalSigma: the cutoff-sample sigma-field of the integral-local information in U of every shell of index at most n.

Main results

• badExtended_subset_iUnion_badScaleEvent: the manuscript's own inclusion.
• measurableSet_badScaleEvent_succ_cutoffShellLocal: locality of every positive level.
• closedBall_cubeBasePoint_subset_cubeTreeRegion, shellCoordinateLocalSigma_le_cutoffShellLocalSigma: the two containments that turn the range constants above into locality statements.

References

• ABK26, e.bad.cluster.def and l.percolation.bad.clusters.
• ABK26, l.percolation.bound.general.

The spatial region of the nine-generation descendant tree

def Algsuperdiff.Section3.Provider.Percolation.cubeTreeRegion {d : ℕ} (Q : HCPolySupport.TriadicCube d) : Set (HCPolySupport.Vec d)

The union of the closed cubes of the nine-generation triadic descendant tree of Q. This is exactly the region whose shell data the extended bad event B^*(z + square_j) reads.

Equations

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

theorem Algsuperdiff.Section3.Provider.Percolation.closedBall_cubeBasePoint_subset_cubeTreeRegion {d : ℕ} {Q R : HCPolySupport.TriadicCube d} {i : ℕ} (hi : i ∈ Finset.range 10) (hR : R ∈ HCPolySupport.descendantsAtScale Q (Q.scale - ↑i)) : Metric.closedBall (BadEvents.cubeBasePoint R) (1 / 2 * 3 ^ R.scale) ⊆ cubeTreeRegion Q

The manuscript's scale-resolved bad events

def Algsuperdiff.Section3.Provider.Percolation.badScaleEvent {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) : ℕ → Set (Cutoff.CutoffSample d)

The manuscript's B_L(z + cu_{m-h}) (ABK26), at the cube Q = z + cu_{m-h}. Level 0 collects the local ellipticity failures of the whole nine-generation tree; level l + 1 collects, for each tree member R, the single-shell oscillation event of e.BoscL.def at shell index R.scale + l + 1.

Equations

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

theorem Algsuperdiff.Section3.Provider.Percolation.measurableSet_badScaleEvent {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (l : ℕ) : MeasurableSet (badScaleEvent M Q l)

theorem Algsuperdiff.Section3.Provider.Percolation.badExtended_subset_iUnion_badScaleEvent {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) : BadEvents.badExtended M Q ⊆ ⋃ (l : ℕ), badScaleEvent M Q l

The manuscript's own scale resolution of the extended bad event (ABK26). Nothing is added: the inclusion is e.Bosc.decomp applied inside each member of the nine-generation tree.

The cutoff-sample local sigma-fields

@[reducible, inline]

abbrev Algsuperdiff.Section3.Provider.Percolation.cutoffShellLocalSigma {d : ℕ} (n : ℤ) (U : Set (HCPolySupport.Vec d)) : MeasurableSpace (Cutoff.CutoffSample d)

The cutoff-sample sigma-field carrying the integral-local information in U of every shell of index at most n.

Equations

• Algsuperdiff.Section3.Provider.Percolation.cutoffShellLocalSigma n U = MeasurableSpace.comap Subtype.val (Algsuperdiff.Section3.Cutoff.lowerShellLocalSigma n U)

theorem Algsuperdiff.Section3.Provider.Percolation.shellCoordinateLocalSigma_le_cutoffShellLocalSigma {d : ℕ} {L n : ℤ} (hLn : L ≤ n) (U : Set (HCPolySupport.Vec d)) : BadEvents.shellCoordinateLocalSigma L U ≤ cutoffShellLocalSigma n U

A single shell of index at most n is carried by the lower-shell local sigma-field at n.

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

Locality of every positive level of the site family. The level-l + 1 bad event of the cube Q is measurable for the integral-local information of the shells of index at most Q.scale + l + 1 in the tree region of Q.

The independence input