StepSevenCaccBoundaryGate #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
0. Triadic arithmetic #
1. The positive half: the clamped outer cube at the sharp gate #
theorem
Algsuperdiff.Section4.Provider.Regularity.image_add_wellPlacedCentre_subset_truncatedWindow_succ
{d : ℕ}
{m j : ℤ}
(hjm : j ≤ m)
{z : HCPolySupport.Vec d}
(hz : z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m))
:
(fun (y : HCPolySupport.Vec d) => ExcessDecay.wellPlacedCentre z m j + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d j) ⊆
ExcessDecay.truncatedWindow z m (j + 1)
The clamped outer cube sits inside the next window up. This is where the
right-hand side of the boundary hcacc is read: c + □_j ⊆ U_{j+1}.