Coarse-graining support: Support.Geometry.TriadicPartition

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

@[simp]

theorem HCPolySupport.parentCube_scale {d : ℕ} (Q : TriadicCube d) : (parentCube Q).scale = Q.scale + 1

@[simp]

theorem HCPolySupport.childCube_scale {d : ℕ} (Q : TriadicCube d) (digits : Fin d → Fin 3) : { scale := Q.scale - 1, index := fun (i : Fin d) => 3 * Q.index i + ↑↑(digits i) - 1 }.scale = Q.scale - 1

theorem HCPolySupport.mem_childCubes_iff {d : ℕ} {Q R : TriadicCube d} : R ∈ childCubes Q ↔ ∃ (digits : Fin d → Fin 3), R = { scale := Q.scale - 1, index := fun (i : Fin d) => 3 * Q.index i + ↑↑(digits i) - 1 }

theorem HCPolySupport.childCube_parent {d : ℕ} (Q : TriadicCube d) (digits : Fin d → Fin 3) : parentCube { scale := Q.scale - 1, index := fun (i : Fin d) => 3 * Q.index i + ↑↑(digits i) - 1 } = Q

@[simp]

theorem HCPolySupport.cubeScaleFactor_childCube {d : ℕ} (Q : TriadicCube d) (digits : Fin d → Fin 3) : cubeScaleFactor { scale := Q.scale - 1, index := fun (i : Fin d) => 3 * Q.index i + ↑↑(digits i) - 1 } = cubeScaleFactor Q / 3

theorem HCPolySupport.cubeSet_childCube_subset {d : ℕ} (Q : TriadicCube d) (digits : Fin d → Fin 3) : cubeSet { scale := Q.scale - 1, index := fun (i : Fin d) => 3 * Q.index i + ↑↑(digits i) - 1 } ⊆ cubeSet Q

theorem HCPolySupport.openCubeSet_childCube_subset {d : ℕ} (Q : TriadicCube d) (digits : Fin d → Fin 3) : openCubeSet { scale := Q.scale - 1, index := fun (i : Fin d) => 3 * Q.index i + ↑↑(digits i) - 1 } ⊆ openCubeSet Q

theorem HCPolySupport.childCubes_nonempty {d : ℕ} (Q : TriadicCube d) : (childCubes Q).Nonempty

theorem HCPolySupport.childCubes_card {d : ℕ} (Q : TriadicCube d) : (childCubes Q).card = 3 ^ d

def HCPolySupport.descendantTranslationShift {d : ℕ} (n : ℕ) (z : Fin d → ℤ) : Fin d → ℤ

Translating a depth-n descendant by parent cube indices requires the integer shift to be multiplied by 3^n, because each descendant step lowers the physical scale by a factor of three.

Equations

• HCPolySupport.descendantTranslationShift n z i = 3 ^ n * z i

@[simp]

theorem HCPolySupport.descendantTranslationShift_zero {d : ℕ} (z : Fin d → ℤ) : descendantTranslationShift 0 z = z

theorem HCPolySupport.descendantTranslationShift_succ {d : ℕ} (n : ℕ) (z : Fin d → ℤ) : descendantTranslationShift (n + 1) z = fun (i : Fin d) => 3 * descendantTranslationShift n z i

theorem HCPolySupport.childCubes_translateCube {d : ℕ} (z : Fin d → ℤ) (Q : TriadicCube d) : childCubes (translateCube z Q) = Finset.image (translateCube fun (i : Fin d) => 3 * z i) (childCubes Q)

theorem HCPolySupport.disjoint_childCubes_of_ne {d : ℕ} {Q R : TriadicCube d} (hQR : Q ≠ R) : Disjoint (childCubes Q) (childCubes R)

@[simp]

theorem HCPolySupport.descendantsAtDepth_zero {d : ℕ} (Q : TriadicCube d) : descendantsAtDepth Q 0 = {Q}

@[simp]

theorem HCPolySupport.descendantsAtDepth_succ {d : ℕ} (Q : TriadicCube d) (n : ℕ) : descendantsAtDepth Q (n + 1) = (descendantsAtDepth Q n).biUnion childCubes

theorem HCPolySupport.descendantsAtDepth_one {d : ℕ} (Q : TriadicCube d) : descendantsAtDepth Q 1 = childCubes Q

theorem HCPolySupport.descendantsAtDepth_translateCube {d : ℕ} (z : Fin d → ℤ) (Q : TriadicCube d) (n : ℕ) : descendantsAtDepth (translateCube z Q) n = Finset.image (translateCube (descendantTranslationShift n z)) (descendantsAtDepth Q n)

theorem HCPolySupport.mem_descendantsAtDepth_succ_iff {d : ℕ} {Q R : TriadicCube d} {n : ℕ} : R ∈ descendantsAtDepth Q (n + 1) ↔ ∃ S ∈ descendantsAtDepth Q n, R ∈ childCubes S

theorem HCPolySupport.exists_descendant_ancestor_at_depth {d : ℕ} {Q R : TriadicCube d} (m n : ℕ) (hR : R ∈ descendantsAtDepth Q (m + n)) : ∃ U ∈ descendantsAtDepth Q m, R ∈ descendantsAtDepth U n

Converse to descendant-depth transitivity: a depth m + n descendant factors through a depth-m ancestor.

theorem HCPolySupport.descendantsAtDepth_nonempty {d : ℕ} (Q : TriadicCube d) (n : ℕ) : (descendantsAtDepth Q n).Nonempty

theorem HCPolySupport.descendantsAtDepth_card_succ {d : ℕ} (Q : TriadicCube d) (n : ℕ) : (descendantsAtDepth Q (n + 1)).card = (descendantsAtDepth Q n).card * 3 ^ d

theorem HCPolySupport.descendantsAtDepth_card {d : ℕ} (Q : TriadicCube d) (n : ℕ) : (descendantsAtDepth Q n).card = (3 ^ d) ^ n

theorem HCPolySupport.descendantsAtScale_eq_descendantsAtDepth {d : ℕ} (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) : descendantsAtScale Q k = descendantsAtDepth Q (Q.scale - k).toNat

theorem HCPolySupport.descendantsAtScale_eq_empty {d : ℕ} (Q : TriadicCube d) {k : ℤ} (hk : Q.scale < k) : descendantsAtScale Q k = ∅

theorem HCPolySupport.descendantsAtScale_translateCube {d : ℕ} (z : Fin d → ℤ) (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) : descendantsAtScale (translateCube z Q) k = Finset.image (translateCube (descendantTranslationShift (Q.scale - k).toNat z)) (descendantsAtScale Q k)

@[simp]

theorem HCPolySupport.descendantsAtScale_self {d : ℕ} (Q : TriadicCube d) : descendantsAtScale Q Q.scale = {Q}

theorem HCPolySupport.mem_descendantsAtScale_iff {d : ℕ} {Q R : TriadicCube d} {k : ℤ} (hk : k ≤ Q.scale) : R ∈ descendantsAtScale Q k ↔ R ∈ descendantsAtDepth Q (Q.scale - k).toNat

theorem HCPolySupport.descendantsAtScale_nonempty {d : ℕ} (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) : (descendantsAtScale Q k).Nonempty

theorem HCPolySupport.not_mem_descendantsAtScale_of_lt {d : ℕ} {Q R : TriadicCube d} {k : ℤ} (hk : Q.scale < k) : R ∉ descendantsAtScale Q k

theorem HCPolySupport.child_scale_of_mem_childCubes {d : ℕ} {Q R : TriadicCube d} (hR : R ∈ childCubes Q) : R.scale = Q.scale - 1

theorem HCPolySupport.parent_scale_of_mem_childCubes {d : ℕ} {Q R : TriadicCube d} (hR : R ∈ childCubes Q) : (parentCube R).scale = Q.scale

theorem HCPolySupport.cubeSet_subset_of_mem_childCubes {d : ℕ} {Q R : TriadicCube d} (hR : R ∈ childCubes Q) : cubeSet R ⊆ cubeSet Q

theorem HCPolySupport.openCubeSet_subset_of_mem_childCubes {d : ℕ} {Q R : TriadicCube d} (hR : R ∈ childCubes Q) : openCubeSet R ⊆ openCubeSet Q

theorem HCPolySupport.disjoint_cubeSet_childCube_of_ne {d : ℕ} (Q : TriadicCube d) {digits₁ digits₂ : Fin d → Fin 3} (hneq : digits₁ ≠ digits₂) : Disjoint (cubeSet { scale := Q.scale - 1, index := fun (i : Fin d) => 3 * Q.index i + ↑↑(digits₁ i) - 1 }) (cubeSet { scale := Q.scale - 1, index := fun (i : Fin d) => 3 * Q.index i + ↑↑(digits₂ i) - 1 })

theorem HCPolySupport.disjoint_cubeSet_of_ne_mem_childCubes {d : ℕ} {Q R S : TriadicCube d} (hR : R ∈ childCubes Q) (hS : S ∈ childCubes Q) (hneq : R ≠ S) : Disjoint (cubeSet R) (cubeSet S)

theorem HCPolySupport.pairwiseDisjoint_childCubes {d : ℕ} (Q : TriadicCube d) : (↑(childCubes Q)).PairwiseDisjoint cubeSet

theorem HCPolySupport.pairwiseDisjoint_descendantsAtDepth {d : ℕ} (Q : TriadicCube d) (n : ℕ) : (↑(descendantsAtDepth Q n)).PairwiseDisjoint cubeSet

theorem HCPolySupport.cubeSet_subset_of_mem_descendantsAtDepth {d : ℕ} {Q R : TriadicCube d} {n : ℕ} : R ∈ descendantsAtDepth Q n → cubeSet R ⊆ cubeSet Q

theorem HCPolySupport.openCubeSet_subset_of_mem_descendantsAtDepth {d : ℕ} {Q R : TriadicCube d} {n : ℕ} : R ∈ descendantsAtDepth Q n → openCubeSet R ⊆ openCubeSet Q

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

theorem HCPolySupport.scale_eq_sub_of_mem_descendantsAtDepth {d : ℕ} {Q R : TriadicCube d} {n : ℕ} : R ∈ descendantsAtDepth Q n → R.scale = Q.scale - ↑n

theorem HCPolySupport.cubeScaleFactor_descendant_eq_div_pow {d : ℕ} {Q R : TriadicCube d} {n : ℕ} (hR : R ∈ descendantsAtDepth Q n) : cubeScaleFactor R = cubeScaleFactor Q / 3 ^ n

theorem HCPolySupport.scale_eq_sub_of_mem_descendantsAtScale {d : ℕ} {Q R : TriadicCube d} {k : ℤ} (hk : k ≤ Q.scale) (hR : R ∈ descendantsAtScale Q k) : R.scale = Q.scale - ↑(Q.scale - k).toNat

theorem HCPolySupport.exists_mem_childCubes_of_mem_cubeSet {d : ℕ} {Q : TriadicCube d} {x : Vec d} (hx : x ∈ cubeSet Q) : ∃ R ∈ childCubes Q, x ∈ cubeSet R

theorem HCPolySupport.cubeSet_subset_iUnion_childCubes {d : ℕ} (Q : TriadicCube d) : cubeSet Q ⊆ ⋃ R ∈ ↑(childCubes Q), cubeSet R

theorem HCPolySupport.iUnion_childCubes_subset_cubeSet {d : ℕ} (Q : TriadicCube d) : ⋃ R ∈ ↑(childCubes Q), cubeSet R ⊆ cubeSet Q

theorem HCPolySupport.cubeSet_eq_iUnion_childCubes {d : ℕ} (Q : TriadicCube d) : cubeSet Q = ⋃ R ∈ ↑(childCubes Q), cubeSet R

theorem HCPolySupport.exists_mem_descendantsAtDepth_of_mem_cubeSet {d : ℕ} {Q : TriadicCube d} {x : Vec d} (n : ℕ) : x ∈ cubeSet Q → ∃ R ∈ descendantsAtDepth Q n, x ∈ cubeSet R

theorem HCPolySupport.cubeSet_subset_iUnion_descendantsAtDepth {d : ℕ} (Q : TriadicCube d) (n : ℕ) : cubeSet Q ⊆ ⋃ R ∈ ↑(descendantsAtDepth Q n), cubeSet R

theorem HCPolySupport.iUnion_descendantsAtDepth_subset_cubeSet {d : ℕ} (Q : TriadicCube d) (n : ℕ) : ⋃ R ∈ ↑(descendantsAtDepth Q n), cubeSet R ⊆ cubeSet Q

theorem HCPolySupport.cubeSet_eq_iUnion_descendantsAtDepth {d : ℕ} (Q : TriadicCube d) (n : ℕ) : cubeSet Q = ⋃ R ∈ ↑(descendantsAtDepth Q n), cubeSet R

theorem HCPolySupport.cubeSet_subset_iUnion_descendantsAtScale {d : ℕ} (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) : cubeSet Q ⊆ ⋃ R ∈ ↑(descendantsAtScale Q k), cubeSet R

theorem HCPolySupport.iUnion_descendantsAtScale_subset_cubeSet {d : ℕ} (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) : ⋃ R ∈ ↑(descendantsAtScale Q k), cubeSet R ⊆ cubeSet Q

theorem HCPolySupport.cubeSet_eq_iUnion_descendantsAtScale {d : ℕ} (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) : cubeSet Q = ⋃ R ∈ ↑(descendantsAtScale Q k), cubeSet R

theorem HCPolySupport.pairwiseDisjoint_descendantsAtScale {d : ℕ} (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) : (↑(descendantsAtScale Q k)).PairwiseDisjoint cubeSet