CubeControlBoundary

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

Boundary extension for translated unit-cube controls

The J2 observable controls a literal open cube. Since shell fields are continuous, this module extends that control to the canonical half-open cube used by triadic partitions.

theorem Algsuperdiff.Section3.Cutoff.cubeSet_subset_closure_openCubeSet {d : ℕ} (Q : HCPolySupport.TriadicCube d) : HCPolySupport.cubeSet Q ⊆ closure (HCPolySupport.openCubeSet Q)

A canonical half-open triadic cube lies in the closure of its open counterpart.

theorem Algsuperdiff.Section3.Cutoff.matrixOperatorNorm_le_translatedUnitCubeControl_of_mem_cubeSet {d : ℕ} (R : HCPolySupport.TriadicCube d) (hR : R.scale = 0) (j : Frozen.Assumptions.ShellField d) {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.cubeSet R) : HCPolySupport.Book.Ch02.matrixOperatorNorm ((↑j).1 x) ≤ translatedUnitCubeControl (HCPolySupport.triadicCubeShift R) j

The continuous matrix operator norm is bounded by the translated unit control on the whole half-open unit cube.