Coarse-graining support: Support.Geometry.TriadicCube

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

structure HCPolySupport.TriadicCube (d : ℕ) : Type

A triadic cube specified by an integer scale and an integer lattice index.

• scale : ℤ

  The integer exponent determining the cube's side length 3 ^ scale.

• index : Fin d → ℤ

  The integer lattice coordinates locating the cube at its scale.

@[instance_reducible]

instance HCPolySupport.instDecidableEqTriadicCube {d✝ : ℕ} : DecidableEq (TriadicCube d✝)

Equations

• HCPolySupport.instDecidableEqTriadicCube = HCPolySupport.instDecidableEqTriadicCube.decEq

def HCPolySupport.instDecidableEqTriadicCube.decEq {d✝ : ℕ} (x✝ x✝¹ : TriadicCube d✝) : Decidable (x✝ = x✝¹)

Equations

• HCPolySupport.instDecidableEqTriadicCube.decEq { scale := a, index := a_1 } { scale := b, index := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def HCPolySupport.instReprTriadicCube.repr {d✝ : ℕ} : TriadicCube d✝ → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance HCPolySupport.instReprTriadicCube {d✝ : ℕ} : Repr (TriadicCube d✝)

Equations

• HCPolySupport.instReprTriadicCube = { reprPrec := HCPolySupport.instReprTriadicCube.repr }

instance HCPolySupport.instCountableTriadicCube (d : ℕ) : Countable (TriadicCube d)

noncomputable def HCPolySupport.cubeScaleFactor {d : ℕ} (Q : TriadicCube d) : ℝ

The cube's side length 3 ^ Q.scale.

Equations

• HCPolySupport.cubeScaleFactor Q = 3 ^ Q.scale

def HCPolySupport.cubeSet {d : ℕ} (Q : TriadicCube d) : Set (Vec d)

Half-open realization of a triadic cube, used for exact cube partitions.

Equations

• One or more equations did not get rendered due to their size.

def HCPolySupport.openCubeSet {d : ℕ} (Q : TriadicCube d) : Set (Vec d)

Open realization of a triadic cube, used when analytic lemmas require open domains.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.isBounded_cubeSet {d : ℕ} (Q : TriadicCube d) : Bornology.IsBounded (cubeSet Q)

A triadic cube is bounded as a subset of the ambient finite-dimensional space.

theorem HCPolySupport.isBounded_openCubeSet {d : ℕ} (Q : TriadicCube d) : Bornology.IsBounded (openCubeSet Q)

An open triadic cube is bounded as a subset of the ambient finite-dimensional space.

def HCPolySupport.originCube (d : ℕ) (m : ℤ) : TriadicCube d

The centered triadic cube descriptor at scale 3^m.

Its source-facing realization openCubeSet (originCube d m) is (-3^m / 2, 3^m / 2)^d. The half-open cubeSet realization is the internal partition representative.

Equations

• HCPolySupport.originCube d m = { scale := m, index := 0 }

def HCPolySupport.translateCube {d : ℕ} (shift : Fin d → ℤ) (Q : TriadicCube d) : TriadicCube d

Shift the lattice index of a cube while preserving its scale.

Equations

• HCPolySupport.translateCube shift Q = { scale := Q.scale, index := fun (i : Fin d) => Q.index i + shift i }

@[simp]

theorem HCPolySupport.cubeScaleFactor_originCube {d : ℕ} (m : ℤ) : cubeScaleFactor (originCube d m) = 3 ^ m

@[simp]

theorem HCPolySupport.cubeScaleFactor_translateCube {d : ℕ} (shift : Fin d → ℤ) (Q : TriadicCube d) : cubeScaleFactor (translateCube shift Q) = cubeScaleFactor Q

@[simp]

theorem HCPolySupport.mem_cubeSet_originCube_iff {d : ℕ} {m : ℤ} {x : Vec d} : x ∈ cubeSet (originCube d m) ↔ ∀ (i : Fin d), -(1 / 2) * 3 ^ m ≤ x i ∧ x i < 1 / 2 * 3 ^ m

@[simp]

theorem HCPolySupport.mem_openCubeSet_originCube_iff {d : ℕ} {m : ℤ} {x : Vec d} : x ∈ openCubeSet (originCube d m) ↔ ∀ (i : Fin d), -(1 / 2) * 3 ^ m < x i ∧ x i < 1 / 2 * 3 ^ m

@[simp]

theorem HCPolySupport.mem_cubeSet_translateCube_iff {d : ℕ} {shift : Fin d → ℤ} {Q : TriadicCube d} {x : Vec d} : x ∈ cubeSet (translateCube shift Q) ↔ (x - fun (i : Fin d) => ↑(shift i) * cubeScaleFactor Q) ∈ cubeSet Q

@[simp]

theorem HCPolySupport.mem_openCubeSet_translateCube_iff {d : ℕ} {shift : Fin d → ℤ} {Q : TriadicCube d} {x : Vec d} : x ∈ openCubeSet (translateCube shift Q) ↔ (x - fun (i : Fin d) => ↑(shift i) * cubeScaleFactor Q) ∈ openCubeSet Q

def HCPolySupport.parentCube {d : ℕ} (Q : TriadicCube d) : TriadicCube d

The cube one scale larger, with index (Q.index + 1) / 3 rounded down coordinatewise.

Equations

• HCPolySupport.parentCube Q = { scale := Q.scale + 1, index := fun (i : Fin d) => (Q.index i + 1).ediv 3 }

def HCPolySupport.childCubes {d : ℕ} (Q : TriadicCube d) : Finset (TriadicCube d)

The 3 ^ d children one scale smaller, indexed by the three digits in each coordinate.

Equations

• HCPolySupport.childCubes Q = Finset.image (fun (digits : Fin d → Fin 3) => { scale := Q.scale - 1, index := fun (i : Fin d) => 3 * Q.index i + ↑↑(digits i) - 1 }) Finset.univ

def HCPolySupport.descendantsAtDepth {d : ℕ} (Q : TriadicCube d) : ℕ → Finset (TriadicCube d)

The finite set obtained by taking children recursively n times, starting with Q.

Equations

• HCPolySupport.descendantsAtDepth Q 0 = {Q}
• HCPolySupport.descendantsAtDepth Q n.succ = (HCPolySupport.descendantsAtDepth Q n).biUnion HCPolySupport.childCubes

def HCPolySupport.descendantsAtScale {d : ℕ} (Q : TriadicCube d) (k : ℤ) : Finset (TriadicCube d)

The descendants of Q at scale k, or the empty set when k > Q.scale.

Equations

• HCPolySupport.descendantsAtScale Q k = if _h : k ≤ Q.scale then HCPolySupport.descendantsAtDepth Q (Q.scale - k).toNat else ∅

noncomputable def HCPolySupport.cubeVolume {d : ℕ} (Q : TriadicCube d) : ℝ

The side length of the cube raised to the dimension.

Equations

• HCPolySupport.cubeVolume Q = HCPolySupport.cubeScaleFactor Q ^ d