Coarse-graining support: Support.Geometry.CubeColoring

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

@[reducible, inline]

abbrev HCPolySupport.CubeColor (d : ℕ) : Type

A triadic color is a choice of residue class modulo 3 in each coordinate.

Equations

• HCPolySupport.CubeColor d = (Fin d → Fin 3)

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

The color of a triadic cube, given by the coordinatewise residue class of its lattice index modulo 3.

Equations

• HCPolySupport.cubeColor Q i = ⟨(Q.index i % 3).toNat, ⋯⟩

def HCPolySupport.descendantsAtScaleColorClass {d : ℕ} (Q : TriadicCube d) (k : ℤ) (c : CubeColor d) : Finset (TriadicCube d)

The descendants of Q at scale k with the prescribed triadic color c.

Equations

• HCPolySupport.descendantsAtScaleColorClass Q k c = {R ∈ HCPolySupport.descendantsAtScale Q k | HCPolySupport.cubeColor R = c}

@[simp]

theorem HCPolySupport.cubeColor_val {d : ℕ} (Q : TriadicCube d) (i : Fin d) : ↑(cubeColor Q i) = (Q.index i % 3).toNat

theorem HCPolySupport.cubeColor_eq_iff_modEq {d : ℕ} {R S : TriadicCube d} : cubeColor R = cubeColor S ↔ ∀ (i : Fin d), R.index i ≡ S.index i [ZMOD 3]

@[simp]

theorem HCPolySupport.mem_descendantsAtScaleColorClass_iff {d : ℕ} {Q R : TriadicCube d} {k : ℤ} {c : CubeColor d} : R ∈ descendantsAtScaleColorClass Q k c ↔ R ∈ descendantsAtScale Q k ∧ cubeColor R = c

theorem HCPolySupport.mem_descendantsAtScaleColorClass_self {d : ℕ} {Q R : TriadicCube d} {k : ℤ} (hR : R ∈ descendantsAtScale Q k) : R ∈ descendantsAtScaleColorClass Q k (cubeColor R)

theorem HCPolySupport.card_cubeColor (d : ℕ) : Fintype.card (CubeColor d) = 3 ^ d

theorem HCPolySupport.card_image_cubeColor_descendantsAtScale_le {d : ℕ} (Q : TriadicCube d) (k : ℤ) : (Finset.image cubeColor (descendantsAtScale Q k)).card ≤ 3 ^ d

theorem HCPolySupport.descendantsAtScale_eq_biUnion_colorClass {d : ℕ} (Q : TriadicCube d) (k : ℤ) : Finset.univ.biUnion (descendantsAtScaleColorClass Q k) = descendantsAtScale Q k

theorem HCPolySupport.descendantsAtScale_eq_biUnion_image_cubeColor {d : ℕ} (Q : TriadicCube d) (k : ℤ) : (Finset.image cubeColor (descendantsAtScale Q k)).biUnion (descendantsAtScaleColorClass Q k) = descendantsAtScale Q k

theorem HCPolySupport.disjoint_descendantsAtScaleColorClass_of_ne {d : ℕ} (Q : TriadicCube d) (k : ℤ) {c₁ c₂ : CubeColor d} (hneq : c₁ ≠ c₂) : Disjoint (descendantsAtScaleColorClass Q k c₁) (descendantsAtScaleColorClass Q k c₂)

theorem HCPolySupport.card_descendantsAtScale_eq_sum_card_colorClass_image {d : ℕ} (Q : TriadicCube d) (k : ℤ) : (descendantsAtScale Q k).card = ∑ c ∈ Finset.image cubeColor (descendantsAtScale Q k), (descendantsAtScaleColorClass Q k c).card

theorem HCPolySupport.scale_le_of_mem_descendantsAtScale {d : ℕ} {Q R : TriadicCube d} {k : ℤ} (hR : R ∈ descendantsAtScale Q k) : k ≤ Q.scale

theorem HCPolySupport.scale_eq_of_mem_descendantsAtScale {d : ℕ} {Q R : TriadicCube d} {k : ℤ} (hR : R ∈ descendantsAtScale Q k) : R.scale = k

theorem HCPolySupport.disjoint_cubeSet_of_scale_eq_of_ne {d : ℕ} {R S : TriadicCube d} (hscale : R.scale = S.scale) (hneq : R ≠ S) : Disjoint (cubeSet R) (cubeSet S)

theorem HCPolySupport.disjoint_cubeSet_of_ne_of_mem_descendantsAtScale {d : ℕ} {Q R S : TriadicCube d} {k : ℤ} (hR : R ∈ descendantsAtScale Q k) (hS : S ∈ descendantsAtScale Q k) (hneq : R ≠ S) : Disjoint (cubeSet R) (cubeSet S)

theorem HCPolySupport.disjoint_cubeSet_of_ne_of_mem_descendantsAtScaleColorClass {d : ℕ} {Q R S : TriadicCube d} {k : ℤ} {c : CubeColor d} (hR : R ∈ descendantsAtScaleColorClass Q k c) (hS : S ∈ descendantsAtScaleColorClass Q k c) (hneq : R ≠ S) : Disjoint (cubeSet R) (cubeSet S)

theorem HCPolySupport.cubeScaleFactor_le_dist_of_ne_of_mem_descendantsAtScaleColorClass {d : ℕ} {Q R S : TriadicCube d} {k : ℤ} {c : CubeColor d} (hR : R ∈ descendantsAtScaleColorClass Q k c) (hS : S ∈ descendantsAtScaleColorClass Q k c) (hneq : R ≠ S) {x y : Vec d} (hx : x ∈ cubeSet R) (hy : y ∈ cubeSet S) : cubeScaleFactor R ≤ dist x y

theorem HCPolySupport.one_le_dist_of_ne_of_mem_descendantsAtScaleColorClass {d : ℕ} {Q R S : TriadicCube d} {k : ℤ} {c : CubeColor d} (hk : 0 ≤ k) (hR : R ∈ descendantsAtScaleColorClass Q k c) (hS : S ∈ descendantsAtScaleColorClass Q k c) (hneq : R ≠ S) {x y : Vec d} (hx : x ∈ cubeSet R) (hy : y ∈ cubeSet S) : 1 ≤ dist x y

theorem HCPolySupport.pairwiseDisjoint_descendantsAtScaleColorClass {d : ℕ} (Q : TriadicCube d) (k : ℤ) (c : CubeColor d) : (↑(descendantsAtScaleColorClass Q k c)).PairwiseDisjoint cubeSet