CubeAxisBridge

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

The translated triadic cube as an axis cube

The localized Dirichlet problems are indexed by the translated triadic cube cubeSetAt y n, the open cube of side 3 ^ n centred at y, while the boundary regularity theory is stated for the axis cube axisCube z L, the open box z + (0, L) ^ d. The two carriers agree once the centre is converted into the lower corner.

The other hypothesis the variational theory asks of this carrier, IsOpenBoundedConvexDomain (cubeSetAt y n), is already available as isOpenBoundedConvexDomain_cubeSetAt; it is recorded here as the sole remaining geometric input of the whole-space comparison on a triadic cube.

theorem Algsuperdiff.Section5.Support.cubeSetAt_eq_axisCube {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) : cubeSetAt y n = HCPolySupport.axisCube (fun (i : Fin d) => y i - 3 ^ n / 2) (3 ^ n)

The translated triadic cube is an axis cube. Its lower corner is the centre shifted by half the side length.