Translations from centered triadic cubes

This file records the elementary geometry identifying an arbitrary triadic cube with a translate of the centered cube at the same scale, and the centered cube at any scale with a positive dilation of the unit centered cube.

noncomputable def Homogenization.triadicCubeShift {d : ℕ} (Q : TriadicCube d) : Vec d

Translation vector carrying the centered cube of scale Q.scale to Q.

Equations

• Homogenization.triadicCubeShift Q i = ↑(Q.index i) * Homogenization.cubeScaleFactor Q

theorem Homogenization.cubeSet_eq_translateSet_originCube_of_triadicCube {d : ℕ} (Q : TriadicCube d) : cubeSet Q = translateSet (triadicCubeShift Q) (cubeSet (originCube d Q.scale))

theorem Homogenization.openCubeSet_eq_translateSet_originCube_of_triadicCube {d : ℕ} (Q : TriadicCube d) : openCubeSet Q = translateSet (triadicCubeShift Q) (openCubeSet (originCube d Q.scale))

theorem Homogenization.openCubeSet_originCube_eq_smul_originCube_zero {d : ℕ} (m : ℤ) : openCubeSet (originCube d m) = cubeScaleFactor (originCube d m) • openCubeSet (originCube d 0)

theorem Homogenization.openCubeSet_eq_translateSet_smul_originCube_zero {d : ℕ} (Q : TriadicCube d) : openCubeSet Q = translateSet (triadicCubeShift Q) (cubeScaleFactor Q • openCubeSet (originCube d 0))