Triadic Cube

Support for the Armstrong–Vicol anomalous-diffusion formalization.

structure Homogenization.TriadicCube (d : ℕ) : Type

Triadic cube described by its integer scale and integer coordinate index.

• scale : ℤ

  Integer scale of the triadic cube, whose side length is three to this power.

• index : Fin d → ℤ

  Integer coordinate index locating the triadic cube at its scale.

@[instance_reducible]

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

Equations

• Homogenization.instDecidableEqTriadicCube = Homogenization.instDecidableEqTriadicCube.decEq

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

Equations

• Homogenization.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 Homogenization.instReprTriadicCube.repr {d✝ : ℕ} : TriadicCube d✝ → ℕ → Std.Format

Equations

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

@[instance_reducible]

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

Equations

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

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

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

Side length of a triadic cube.

Equations

• Homogenization.cubeScaleFactor Q = 3 ^ Q.scale

def Homogenization.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 Homogenization.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 Homogenization.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 Homogenization.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 Homogenization.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

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

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

Translate the integer index of a triadic cube while preserving its scale.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

theorem Homogenization.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 Homogenization.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 Homogenization.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 Homogenization.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 Homogenization.parentCube {d : ℕ} (Q : TriadicCube d) : TriadicCube d

Unique triadic parent at the next coarser scale.

Equations

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

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

Finite set of triadic children at the next finer scale.

Equations

• Homogenization.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 Homogenization.descendantsAtDepth {d : ℕ} (Q : TriadicCube d) : ℕ → Finset (TriadicCube d)

Triadic descendants obtained after a specified number of subdivision steps.

Equations

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

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

Triadic descendants at a specified finer scale, empty above the cube's scale.

Equations

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

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

Euclidean volume of a triadic cube.

Equations

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