HomSpineDepthStraddleMeasure

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

The straddling-pair ingredient: separation and the boundary-layer measure

What this file is for

The Gagliardo half of the single-depth dual test (HomSpineCzGridDepthTest §4) needs ONE geometric fact about the depth-j slice g_j = gridDualDepthTest Q j v, a function constant on each depth-j cell:

  g_j(y) ≠ g_j(x)   ⟹   x lies within |x-y| of the depth-j skeleton,

together with the size of that skeleton neighbourhood. Both are proved here.

• gridDualDepthTest_eq_of_mem_cubeShrunkSet — THE SEPARATION. If x sits in the t-shrunk core of its depth-j cell and dist x y < t · (cell side), then g_j(y) = g_j(x). (Half-open triadic cells and the ambient sup metric: a sup-ball of radius t·ℓ around a point of the shrunk core stays inside the cell.)
• volume_cubeBoundaryLayer_le — THE STRADDLING MEASURE, ≤ 2·d·t·|R| per cell, aggregating to ≤ 2·d·t over the whole depth-j skeleton. This is the 3^{j-k}-smallness the near bands of the band reduction run on: at band k ≥ j the relevant thickness is t = 3^{j-k}.

MINING CORRECTION (recorded): the survey reported that CoarseGraining's Geometry/BoundaryLayer carries "no measure bound". It does not, but Geometry/CubeMeasure does — volume_cubeBoundaryLayer_toReal_of_nonneg_le_half computes the layer volume EXACTLY as |R| - ((1-2t)·ℓ)^d. Everything below is that identity plus Bernoulli; no new measure theory is developed.

What is still missing for the band reduction

The remaining ingredients are the tail-kernel integral ∫_{y ∈ Q, |x-y| ≥ r} |x-y|^{-(s·p'+d)} dy ≤ C(d)·(1-3^{-s·p'})⁻¹·r^{-s·p'} and the layer-cake integration of dist(x, skeleton)^{-s·p'} against these measures. See this file report; they are NOT in this file.

1. Separation: the shrunk core does not see the skeleton

theorem Algsuperdiff.Section4.Provider.Homogenization.mem_cubeSet_of_mem_cubeShrunkSet_of_dist_lt {d : ℕ} {R : HCPolySupport.TriadicCube d} {t : ℝ} {x y : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.cubeShrunkSet R t) (hy : dist x y < t * HCPolySupport.cubeScaleFactor R) : y ∈ HCPolySupport.cubeSet R

A sup-ball of radius t·ℓ about a point of the t-shrunk core of a triadic cube stays inside the (half-open) cube.

theorem Algsuperdiff.Section4.Provider.Homogenization.gridDualDepthTest_eq_of_mem_cubeShrunkSet {d : ℕ} (Q : HCPolySupport.TriadicCube d) (j : ℕ) (v : HCPolySupport.TriadicCube d → HCPolySupport.Vec d) {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtDepth Q j) {t : ℝ} {x y : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.cubeShrunkSet R t) (hxt : 0 ≤ t) (hy : dist x y < t * HCPolySupport.cubeScaleFactor R) : gridDualDepthTest Q j v y = gridDualDepthTest Q j v x

THE SEPARATION. A depth-j slice is constant on the t·ℓ-ball around any point of the t-shrunk core of a depth-j cell. Contrapositive: the pairs on which g_j actually jumps have x inside the boundary layer of thickness |x-y|/ℓ — the straddling pairs.

2. The straddling measure

theorem Algsuperdiff.Section4.Provider.Homogenization.volume_cubeBoundaryLayer_le {d : ℕ} (R : HCPolySupport.TriadicCube d) {t : ℝ} (ht0 : 0 ≤ t) (ht : t ≤ 1 / 2) : MeasureTheory.volume (HCPolySupport.cubeBoundaryLayer R t) ≤ ENNReal.ofReal (2 * ↑d * t * HCPolySupport.cubeVolume R)

THE STRADDLING MEASURE BOUND. The boundary layer of normalized thickness t of a triadic cube has volume at most 2·d·t times the cube's volume — the 3^{j-k}-smallness the near bands of the band reduction consume, read at t = 3^{j-k}.

Proof: CoarseGraining's exact layer volume |R| - ((1-2t)·ℓ)^d, plus Bernoulli.