Inflate

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

Inflated bad events on triadic lattice cubes

This file partitions the integer lattice into centered triadic cubes, defines the corresponding inflated bad events, and records the residue colouring used to separate cubes in one colour class.

def Algsuperdiff.Section5.Percolation.cubeCenter {d : ℕ} (L : ℕ) (v : Site d) : Site d

The center indexed by v in the sublattice 3^L ℤ^d.

Equations

• Algsuperdiff.Section5.Percolation.cubeCenter L v i = ↑(3 ^ L) * v i

def Algsuperdiff.Section5.Percolation.centerIndex {d : ℕ} (L : ℕ) (z : Site d) : Site d

The canonical index of the centered triadic cube containing z.

Equations

• Algsuperdiff.Section5.Percolation.centerIndex L z i = (z i).bdiv (3 ^ L)

def Algsuperdiff.Section5.Percolation.centeredRemainder {d : ℕ} (L : ℕ) (z : Site d) : Site d

The centered remainder of z modulo 3^L, coordinatewise.

Equations

• Algsuperdiff.Section5.Percolation.centeredRemainder L z i = (z i).bmod (3 ^ L)

theorem Algsuperdiff.Section5.Percolation.cubeCenter_add_centeredRemainder {d L : ℕ} (z : Site d) : cubeCenter L (centerIndex L z) + centeredRemainder L z = z

A site is its canonical triadic center plus its centered remainder.

theorem Algsuperdiff.Section5.Percolation.centeredRemainder_inCube {d L : ℕ} (z : Site d) : inCube L (centeredRemainder L z)

The canonical centered remainder lies in the open scale-L cube.

def Algsuperdiff.Section5.Percolation.latticeCubeSites {d : ℕ} (L : ℕ) (v : Site d) : Finset (Site d)

The finite set of sites in the centered scale-L cube indexed by v.

Equations

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

theorem Algsuperdiff.Section5.Percolation.mem_latticeCubeSites_centerIndex {d L : ℕ} (z : Site d) : z ∈ latticeCubeSites L (centerIndex L z)

Every site lies in its canonical centered triadic cube.

theorem Algsuperdiff.Section5.Percolation.card_latticeCubeSites (d L : ℕ) (v : Site d) : (latticeCubeSites L v).card = 3 ^ (d * L)

Every translated scale-L cube has exactly 3^(dL) lattice sites.

def Algsuperdiff.Section5.Percolation.centerColor {d : ℕ} (v : Site d) : Fin d → ZMod 3

The residue colour of a triadic cube index.

Equations

• Algsuperdiff.Section5.Percolation.centerColor v i = ↑(v i)

theorem Algsuperdiff.Section5.Percolation.centerIndex_eq_of_mem_latticeCubeSites {d L : ℕ} {v z : Site d} (hz : z ∈ latticeCubeSites L v) : centerIndex L z = v

A site belongs to only its canonical centered triadic cube.

theorem Algsuperdiff.Section5.Percolation.mem_latticeCubeSites_iff_centerIndex_eq {d L : ℕ} {v z : Site d} : z ∈ latticeCubeSites L v ↔ centerIndex L z = v

Cube membership is characterized by the canonical cube index.

theorem Algsuperdiff.Section5.Percolation.natAbs_centerIndex_sub_le_one_of_siteDist_lt {d L : ℕ} {z y : Site d} (hzy : siteDist z y < 3 ^ L) (i : Fin d) : (centerIndex L z i - centerIndex L y i).natAbs ≤ 1

Sites at sup distance strictly less than 3^L have canonical scale-L cube indices differing by at most one in every coordinate.

theorem Algsuperdiff.Section5.Percolation.siteDist_cubeCenter_le_half {d L : ℕ} {v z : Site d} (hz : z ∈ latticeCubeSites L v) : siteDist (cubeCenter L v) z ≤ 3 ^ L / 2

Every site of a translated scale-L cube is within sup distance 3^L / 2 of its center.

theorem Algsuperdiff.Section5.Percolation.latticeCubeSites_separated_of_sameColor {d L : ℕ} {v w : Site d} (hvw : v ≠ w) (hcolor : centerColor v = centerColor w) {z y : Site d} (hz : z ∈ latticeCubeSites L v) (hy : y ∈ latticeCubeSites L w) : 3 ^ L < siteDist z y

Distinct triadic cubes of one residue colour are separated by more than their scale. This is the geometric input for within-colour independence.

def Algsuperdiff.Section5.Percolation.inflatedBadEvent {Ω : Type u_1} {d : ℕ} (B : ℕ → Site d → Set Ω) (L : ℕ) (v : Site d) : Set Ω

The scale-L bad event inflated over one triadic cube.

Equations

• Algsuperdiff.Section5.Percolation.inflatedBadEvent B L v = ⋃ z ∈ Algsuperdiff.Section5.Percolation.latticeCubeSites L v, B L z

def Algsuperdiff.Section5.Percolation.inflatedBadSet {Ω : Type u_1} {d : ℕ} (B : ℕ → Site d → Set Ω) (z : Site d) : Set Ω

The union, over all scales, of the inflated cube event containing z.

Equations

• Algsuperdiff.Section5.Percolation.inflatedBadSet B z = ⋃ (L : ℕ), Algsuperdiff.Section5.Percolation.inflatedBadEvent B L (Algsuperdiff.Section5.Percolation.centerIndex L z)

theorem Algsuperdiff.Section5.Percolation.badSet_subset_inflatedBadSet {Ω : Type u_1} {d : ℕ} (B : ℕ → Site d → Set Ω) (z : Site d) : badSet B z ⊆ inflatedBadSet B z

The original bad event at a site is contained in its inflated version.

theorem Algsuperdiff.Section5.Percolation.measurableSet_inflatedBadEvent {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} {B : ℕ → Site d → Set Ω} (hB : ∀ (L : ℕ) (z : Site d), MeasurableSet (B L z)) (L : ℕ) (v : Site d) : MeasurableSet (inflatedBadEvent B L v)

Inflated bad events are measurable when every original bad event is.

theorem Algsuperdiff.Section5.Percolation.measureReal_inflatedBadEvent_le {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (P : MeasureTheory.Measure Ω) (B : ℕ → Site d → Set Ω) (a T : ℝ) (hB : ∀ (L : ℕ) (z : Site d), P.real (B L z) ≤ Real.exp (-(T ^ 2 * 3 ^ (a * ↑L)))) (L : ℕ) (v : Site d) : P.real (inflatedBadEvent B L v) ≤ 3 ^ (d * L) * Real.exp (-(T ^ 2 * 3 ^ (a * ↑L)))

A union bound for one inflated cube, retaining the exact cube-cardinality factor.

theorem Algsuperdiff.Section5.Percolation.measureReal_inflatedBadEvent_le_exp_half {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (P : MeasureTheory.Measure Ω) (B : ℕ → Site d → Set Ω) (a T : ℝ) (hB : ∀ (L : ℕ) (z : Site d), P.real (B L z) ≤ Real.exp (-(T ^ 2 * 3 ^ (a * ↑L)))) (ha : 1 ≤ a) (hT : 2 * (↑d + 1) ≤ T) (L : ℕ) (v : Site d) : P.real (inflatedBadEvent B L v) ≤ Real.exp (-(T ^ 2 * 3 ^ (a * ↑L) / 2))

Once T exceeds a dimension-only threshold, the polynomial cube-volume factor is absorbed into half of the stretched-exponential exponent.

theorem Algsuperdiff.Section5.Percolation.iIndepFun_inflatedIndicator_of_sameColor {Ω : Type u_1} [MeasurableSpace Ω] {d L : ℕ} (P : MeasureTheory.Measure Ω) (B : ℕ → Site d → Set Ω) (hsep : SepIndep P B) (hB : ∀ (L : ℕ) (z : Site d), MeasurableSet (B L z)) (s : Finset (Site d)) (b : Fin d → ZMod 3) (hcolor : ∀ v ∈ s, centerColor v = b) : ProbabilityTheory.iIndepFun (fun (v : ↥s) => (inflatedBadEvent B L ↑v).indicator fun (_ω : Ω) => 1) P

Inflated-event indicators over finitely many cubes of one residue colour are mutually independent.

def Algsuperdiff.Section5.Percolation.touchingCenters {d : ℕ} (L : ℕ) (Γ : List (Site d)) : Finset (Site d)

The finite set of canonical scale-L cube indices touched by a path.

Equations

• Algsuperdiff.Section5.Percolation.touchingCenters L Γ = Finset.image (Algsuperdiff.Section5.Percolation.centerIndex L) Γ.toFinset

theorem Algsuperdiff.Section5.Percolation.centerIndex_mem_touchingCenters {d L : ℕ} {Γ : List (Site d)} {z : Site d} (hz : z ∈ Γ) : centerIndex L z ∈ touchingCenters L Γ

A path vertex contributes its canonical cube to touchingCenters.

noncomputable def Algsuperdiff.Section5.Percolation.inflatedCubeCount {Ω : Type u_1} {d : ℕ} (B : ℕ → Site d → Set Ω) (L : ℕ) (Γ : List (Site d)) (ω : Ω) : ℕ

The number of touched scale-L cubes whose inflated event occurs.

Equations

• Algsuperdiff.Section5.Percolation.inflatedCubeCount B L Γ ω = {v ∈ Algsuperdiff.Section5.Percolation.touchingCenters L Γ | ω ∈ Algsuperdiff.Section5.Percolation.inflatedBadEvent B L v}.card