LayerDensity

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

l.bad.cubes.density: the density of bad cubes in a Whitney layer

∑_{□ ∈ 𝒲(□_m,n) ∩ ℐ} |□| / |□_m|  ≤  exp(-c E^{-2} γ^{-1}) + 3^{-(n+h_n)/2} .

Why the mass form

The printed display is

3^{-n} ⨍_{□ ∈ 𝒲(□_m,n)} 1_{𝓑(□)}  ≤  exp(-c E^{-2} γ^{-1}) + 3^{-(n+h_n)/2}

and its proof is exactly: 𝒲(□_m,n) ⊆ {z + □_{m-n-h_n}: z ∈ 3^{m-n-h_n} ℤ^d ∩ □_m}, 𝓑 ⊆ 𝓑^*, then e.density.deterministic at h = n + h_n. What that argument produces is the ambient density — the bad mass of the layer relative to □_m — and the 3^{-n} prefactor is precisely the layer's own volume fraction, already spent. The literal 3^{-n} ⨍_{𝒲(□_m,n)} reading is not delivered here: it requires #𝒲(□_m,n) ≥ 3^{-n}·3^{d(n+h_n)}, which fails at n = 1 (where #𝒲(□_m,1) = 3^{d h_1} and 3^{-1}·3^{d(1+h_1)} = 3^{d-1}·3^{d h_1}) and at small n for large d.

Where the constant comes from

Percolation.scaleSeparationDensityThreshold M E h is exp(-(c(d) E^{-2} γ^{-1})) + 3^{-h/2} with the dimension-only witness c(d) = siteRateBase d / 2 supplied by the proved density conclusion; this is the right side of e.bad.cubes.density read at h = n + h_n.

Main results

• cubeMassRatio: |R| / |Q| for triadic cubes.
• sum_cubeMassRatio_badFamilyLayer_le: e.bad.cubes.density in mass form.

References

• ABK26, l.bad.cubes.density.

Volume fractions

noncomputable def Algsuperdiff.Section3.Provider.Whitney.cubeMassRatio {d : ℕ} (Q R : HCPolySupport.TriadicCube d) : ℝ

|R| / |Q| for triadic cubes: the mass a cube carries inside its root.

Equations

• Algsuperdiff.Section3.Provider.Whitney.cubeMassRatio Q R = (3 ^ d) ^ (R.scale - Q.scale)

theorem Algsuperdiff.Section3.Provider.Whitney.cubeMassRatio_of_mem_descendantsAtDepth {d : ℕ} {Q R : HCPolySupport.TriadicCube d} {h : ℕ} (hR : R ∈ HCPolySupport.descendantsAtDepth Q h) : cubeMassRatio Q R = ((3 ^ d) ^ h)⁻¹

The layer sits inside the base lattice of its own depth

theorem Algsuperdiff.Section3.Provider.Whitney.index_mem_cubeFinset_of_mem_descendantsAtDepth {d : ℕ} {m : ℤ} {h : ℕ} {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtDepth (HCPolySupport.originCube d m) h) : R.index ∈ Percolation.cubeFinset h

The index of a depth-h descendant of □_m is a site of □_h ∩ ℤ^d, i.e. the manuscript's base lattice 3^{m-h} ℤ^d ∩ □_m in the cube-side units of Percolation.cubeFinset.

theorem Algsuperdiff.Section3.Provider.Whitney.siteCube_index_of_mem_descendantsAtDepth {d : ℕ} {m : ℤ} {h : ℕ} {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtDepth (HCPolySupport.originCube d m) h) : Percolation.siteCube (m - ↑h) R.index = R

A depth-h descendant of □_m is the base cube of its own index.

theorem Algsuperdiff.Section3.Provider.Whitney.index_injOn_descendantsAtDepth {d : ℕ} (m : ℤ) (h : ℕ) : Set.InjOn (fun (R : HCPolySupport.TriadicCube d) => R.index) ↑(HCPolySupport.descendantsAtDepth (HCPolySupport.originCube d m) h)

Distinct depth-h descendants of □_m have distinct indices.

The density estimate

theorem Algsuperdiff.Section3.Provider.Whitney.sum_cubeMassRatio_badFamilyLayer_le {d : ℕ} {M : ABKModel d} {m : ℤ} {E b : ℝ} {k₀ : ℕ} {omega : Cutoff.CutoffSample d} (hne : (Percolation.hsepSet M m E b omega).Nonempty) (n : ℕ) : ∑ Q ∈ badFamilyLayer M m (whitneyScale M m E b k₀ omega) n omega, cubeMassRatio (HCPolySupport.originCube d m) Q ≤ Percolation.scaleSeparationDensityThreshold M E (n + whitneyScale M m E b k₀ omega n)

∑_{□ ∈ 𝒲(□_m,n) ∩ ℐ} |□| / |□_m|
  ≤ exp(-c(d) E^{-2} γ^{-1}) + 3^{-(n+h_n)/2} .