Coarse-graining support: Support.Book.Ch04.TriadicCubeTranslation

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

def HCPolySupport.Book.Ch04.scaleTranslationShift {d : ℕ} (k : ℤ) (R : TriadicCube d) : Fin d → ℤ

Integer shift taking a nonnegative-scale origin cube to a cube at the same scale.

Equations

• HCPolySupport.Book.Ch04.scaleTranslationShift k R i = Int.ofNat (3 ^ k.toNat) * R.index i

theorem HCPolySupport.Book.Ch04.cubeSet_eq_translateSet_originCube_of_nonneg_scale {d : ℕ} {R : TriadicCube d} (hk : 0 ≤ R.scale) : cubeSet R = translateSet (intVecToRealVec (scaleTranslationShift R.scale R)) (cubeSet (originCube d R.scale))

At nonnegative scale, every triadic cube is an integer translate of the origin cube at the same scale.

theorem HCPolySupport.Book.Ch04.scale_eq_of_mem_descendantsAtScale_originCube {d : ℕ} {n m : ℤ} {R : TriadicCube d} (hnm : n ≤ m) (hR : R ∈ descendantsAtScale (originCube d m) n) : R.scale = n

Descendants of the origin cube at a fixed scale have that scale.

theorem HCPolySupport.Book.Ch04.cubeSet_eq_translateSet_originCube_of_mem_descendantsAtScale_originCube {d : ℕ} {n m : ℤ} {R : TriadicCube d} (hn : 0 ≤ n) (hnm : n ≤ m) (hR : R ∈ descendantsAtScale (originCube d m) n) : cubeSet R = translateSet (intVecToRealVec (scaleTranslationShift n R)) (cubeSet (originCube d n))

A descendant of a nonnegative-scale origin cube is an integer translate of the origin cube at the descendant scale.