OneStepEvenBoundSlab #

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

The near-face geometry of the one-met-face boundary window #

The boundary branch of the §4.3 excess decay works on the truncated window U₂ = truncatedWindow x m k = coordBox (windowLo x m k) (windowHi x m k) and on its doubled partner R = reflectedWindow x m k, in the regime where exactly one face of ∂□_m meets the closure of U₂, namely the upper i-face {y i = a} with a = ½·3^m.

This module proves the near-face geometry the even (non-odd) part of the comparison estimate consumes:

the core slab S = coordBox (slabLo …) (slabHi …), the layer of depth delta directly under the met face, transversally concentric with the window at half its side: S = (a − delta, a) × ∏_{j ≠ i} (x j − 3^k/4, x j + 3^k/4);
the deep slab D, the core slab pushed one further depth delta away from the face: D = (a − 2delta, a − delta) × ∏_{j ≠ i} (x j − 3^k/4, x j + 3^k/4);
the Taylor box T = (a − 2delta, a + delta) × ∏_{j ≠ i} (x j − 3^k/4, x j + 3^k/4), the slightly larger box that contains the core slab, its delta-translate D, and the reflection of the core slab through the met face;
the sup-ball family: every point of T carries a sup-ball of radius 3^k/4 inside the doubled window R, which is what the interior Hessian estimate consumes on the doubled domain.

The window edges in this regime #

Write a = ½·3^m, w = 3^k and ℓ = windowHi x m k i − windowLo x m k i.

  MeetsUpperFace x m k i  ↔  a ≤ x i + w/2      ⟹  windowHi x m k i = a;
  k < m and the upper i-face met  ⟹  the lower i-face is unmet
                                  ⟹  windowLo x m k i = x i − w/2;
  x ∈ □_m  ⟹  x i < a  ⟹  ℓ = a − x i + w/2 > w/2 ,   and   ℓ ≤ w .

On the unmet coordinates j ≠ i the window keeps its full triadic edge (x j − w/2, x j + w/2) and the reflection does not move it; on the met coordinate the doubled edge is (a − ℓ, a + ℓ), because reflectedLo = windowLo and reflectedHi = 3^m − windowLo = a + ℓ.

With the depth budget 16·delta ≤ w we get 2·delta ≤ w/8 < w/2 < ℓ, which is exactly what makes the three boxes fit: transversally w/4 < w/2, and in the i direction the Taylor box (a − 2delta, a + delta) is inside (a − ℓ, a + ℓ) with a margin of at least w/8 on each side — enough room for a whole sup-ball of radius w/4 around every point of T.

What is not done here #

Nothing analytic. No function is restricted, no Taylor expansion is performed, no Hessian bound is proved. This module is pure geometry: box endpoints, inclusions of boxes, one reflection identity, one ball family, and one lower bound on the Lebesgue measure of the core slab.

References #

ABK26, l.excess.decay.good.scales.
Algsuperdiff.Section4.Provider.ExcessDecay.OddReflectionWindow (the window and its partial reflection), …OddReflectionVolume (volume_coordBox), …OneStepBoundaryGeometry (the dist_pi_lt_iff idiom for sup-balls).
CoarseGraining Homogenization.Sobolev.Foundations.CubeReflection.Reflections (coordFaceReflection).

OneStepEvenBoundSlab #

The near-face geometry of the one-met-face boundary window #

The window edges in this regime #

What is not done here #

References #

1. The window edges in the one-met-face regime #

2. The three near-face boxes #

The six corners, coordinate by coordinate #

3. Nondegeneracy #

4. The slabs sit inside the window #

5. The slabs sit inside the Taylor box #

6. The reflection of the core slab proves in the Taylor box #

7. The sup-ball family on the Taylor box #

8. The core slab's volume from below #