Coarse-graining support: Support.Geometry.ScaleColoring

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

noncomputable def HCPolySupport.scaleColorPeriod (k : ℤ) : ℕ

The Chapter 4 scale-dependent coloring period r_k = 1 + \lceil 3^{-k} \rceil.

Equations

• HCPolySupport.scaleColorPeriod k = 1 + ⌈3 ^ (-k)⌉₊

@[reducible, inline]

abbrev HCPolySupport.ScaleColor (d : ℕ) (k : ℤ) : Type

The scale-dependent triadic colors attached to cubes at scale k.

Equations

• HCPolySupport.ScaleColor d k = (Fin d → Fin (HCPolySupport.scaleColorPeriod k))

theorem HCPolySupport.scaleColorPeriod_pos (k : ℤ) : 0 < scaleColorPeriod k

theorem HCPolySupport.scaleColorPeriod_int_pos (k : ℤ) : 0 < ↑(scaleColorPeriod k)

theorem HCPolySupport.scaleColorPeriod_int_ne_zero (k : ℤ) : ↑(scaleColorPeriod k) ≠ 0

noncomputable def HCPolySupport.cubeScaleColor {d : ℕ} (k : ℤ) (Q : TriadicCube d) : ScaleColor d k

The scale-dependent color of a triadic cube, given by its coordinatewise residue class modulo r_k.

Equations

• HCPolySupport.cubeScaleColor k Q i = ⟨(Q.index i % ↑(HCPolySupport.scaleColorPeriod k)).toNat, ⋯⟩

noncomputable def HCPolySupport.descendantsAtScaleScaleColorClass {d : ℕ} (Q : TriadicCube d) (k : ℤ) (c : ScaleColor d k) : Finset (TriadicCube d)

The descendants of Q at scale k with prescribed scale-dependent color c.

Equations

• HCPolySupport.descendantsAtScaleScaleColorClass Q k c = {R ∈ HCPolySupport.descendantsAtScale Q k | HCPolySupport.cubeScaleColor k R = c}

@[simp]

theorem HCPolySupport.cubeScaleColor_val {d : ℕ} (k : ℤ) (Q : TriadicCube d) (i : Fin d) : ↑(cubeScaleColor k Q i) = (Q.index i % ↑(scaleColorPeriod k)).toNat

theorem HCPolySupport.cubeScaleColor_eq_iff_modEq {d : ℕ} {k : ℤ} {R S : TriadicCube d} : cubeScaleColor k R = cubeScaleColor k S ↔ ∀ (i : Fin d), R.index i ≡ S.index i [ZMOD ↑(scaleColorPeriod k)]

@[simp]

theorem HCPolySupport.mem_descendantsAtScaleScaleColorClass_iff {d : ℕ} {Q R : TriadicCube d} {k : ℤ} {c : ScaleColor d k} : R ∈ descendantsAtScaleScaleColorClass Q k c ↔ R ∈ descendantsAtScale Q k ∧ cubeScaleColor k R = c

theorem HCPolySupport.mem_descendantsAtScaleScaleColorClass_self {d : ℕ} {Q R : TriadicCube d} {k : ℤ} (hR : R ∈ descendantsAtScale Q k) : R ∈ descendantsAtScaleScaleColorClass Q k (cubeScaleColor k R)

theorem HCPolySupport.card_scaleColor (d : ℕ) (k : ℤ) : Fintype.card (ScaleColor d k) = scaleColorPeriod k ^ d

theorem HCPolySupport.card_image_cubeScaleColor_descendantsAtScale_le {d : ℕ} (Q : TriadicCube d) (k : ℤ) : (Finset.image (cubeScaleColor k) (descendantsAtScale Q k)).card ≤ scaleColorPeriod k ^ d

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

theorem HCPolySupport.descendantsAtScale_eq_biUnion_image_cubeScaleColor {d : ℕ} (Q : TriadicCube d) (k : ℤ) : (Finset.image (cubeScaleColor k) (descendantsAtScale Q k)).biUnion (descendantsAtScaleScaleColorClass Q k) = descendantsAtScale Q k

theorem HCPolySupport.disjoint_descendantsAtScaleScaleColorClass_of_ne {d : ℕ} (Q : TriadicCube d) (k : ℤ) {c₁ c₂ : ScaleColor d k} (hneq : c₁ ≠ c₂) : Disjoint (descendantsAtScaleScaleColorClass Q k c₁) (descendantsAtScaleScaleColorClass Q k c₂)

theorem HCPolySupport.card_descendantsAtScale_eq_sum_card_scaleColorClass_image {d : ℕ} (Q : TriadicCube d) (k : ℤ) : (descendantsAtScale Q k).card = ∑ c ∈ Finset.image (cubeScaleColor k) (descendantsAtScale Q k), (descendantsAtScaleScaleColorClass Q k c).card

theorem HCPolySupport.one_le_scaleColorPeriod_pred_mul_zpow (k : ℤ) : 1 ≤ (↑(scaleColorPeriod k) - 1) * 3 ^ k

theorem HCPolySupport.scaleColorPeriod_le_three_mul_one_add_zpow_neg (k : ℤ) : ↑(scaleColorPeriod k) ≤ 3 * (1 + 3 ^ (-k))

theorem HCPolySupport.one_le_dist_of_ne_of_mem_descendantsAtScaleScaleColorClass {d : ℕ} {Q R S : TriadicCube d} {k : ℤ} {c : ScaleColor d k} (hR : R ∈ descendantsAtScaleScaleColorClass Q k c) (hS : S ∈ descendantsAtScaleScaleColorClass 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_descendantsAtScaleScaleColorClass {d : ℕ} (Q : TriadicCube d) (k : ℤ) (c : ScaleColor d k) : (↑(descendantsAtScaleScaleColorClass Q k c)).PairwiseDisjoint cubeSet