Documentation

LeanPool.HighContrastHomogenization.Support.Geometry.TriadicCubeTranslation

Coarse-graining support: Support.Geometry.TriadicCubeTranslation #

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

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.

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

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

Equations
Instances For
    source
    theorem HCPolySupport.cubeSet_eq_translateSet_originCube_of_triadicCube {d : ℕ} (Q : TriadicCube d) :
    cubeSet Q = translateSet (triadicCubeShift Q) (cubeSet (originCube d Q.scale))
    source
    theorem HCPolySupport.openCubeSet_eq_translateSet_originCube_of_triadicCube {d : ℕ} (Q : TriadicCube d) :
    openCubeSet Q = translateSet (triadicCubeShift Q) (openCubeSet (originCube d Q.scale))
    source
    theorem HCPolySupport.openCubeSet_originCube_eq_smul_originCube_zero {d : ℕ} (m : ℤ) :
    openCubeSet (originCube d m) = cubeScaleFactor (originCube d m) • openCubeSet (originCube d 0)
    source
    theorem HCPolySupport.openCubeSet_eq_translateSet_smul_originCube_zero {d : ℕ} (Q : TriadicCube d) :
    openCubeSet Q = translateSet (triadicCubeShift Q) (cubeScaleFactor Q • openCubeSet (originCube d 0))