BoxGeometry

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

Gap scales and snapped centres for axis cubes

This file isolates the finite-dimensional geometry used to pass from estimates centred on cube faces to estimates centred at arbitrary points of the cube.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.axisCube_subset_closureSet {d : ℕ} (z : HCPolySupport.Vec d) (L : ℝ) : HCPolySupport.axisCube z L ⊆ {x : HCPolySupport.Vec d | MemAxisCubeClosure z L x}

Every point of an open axis cube belongs to its coordinatewise closure.