High-contrast homogenization: Provider.Recurrence.AdaptedCell

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Adapted cells as linear images of the standard aligned cubes

An adapted cell ⋄_j^q = q□_j is the image of a centered triadic cube under the grid map, and an aligned adapted cell 3^j q w + ⋄_j^q is the image of the standard aligned cube 3^j w + □_j under the same map. Since a rounded grid is invertible, every incidence question about adapted cells is the corresponding question about standard cubes, transported by an injection.

This file records that transport and the combinatorial clauses of the aligned subdivision in the coarse-block properties taken from HC: an aligned scale-j cell has its center in the scale-p parent exactly when each of its indices is one of the 3^{p-j} admissible ones, such a cell is contained in the parent, distinct aligned cells at the same scale are disjoint, and the admissible indices number 3^{d(p-j)}. That the cells cover the parent up to a null set is proved in the companion file.

The grid map is injective

theorem HCPolySupport.HighContrast.Recurrence.matVecMul_injective {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) : Function.Injective (matVecMul q)

A positive definite grid matrix acts injectively on vectors.

Scale bookkeeping

theorem HCPolySupport.HighContrast.Recurrence.intCast_three_pow_toNat {j p : ℤ} (hjp : j ≤ p) : ↑(3 ^ (p - j).toNat) = 3 ^ (p - j)

The scale ratio between two triadic scales, as an integer.

theorem HCPolySupport.HighContrast.Recurrence.zpow_three_split {j p : ℤ} (hjp : j ≤ p) : 3 ^ p = 3 ^ j * ↑(3 ^ (p - j).toNat)

The parent scale factors through the child scale.

theorem HCPolySupport.HighContrast.Recurrence.odd_three_pow (n : ℕ) : ∃ (m : ℤ), 3 ^ n = 2 * m + 1

The scale ratio is odd, so no index sits on the boundary of the parent.

Membership in the standard aligned cubes

theorem HCPolySupport.HighContrast.Recurrence.mem_centeredCube_iff {d : ℕ} {k : ℤ} {x : Vec d} : x ∈ centeredCube d k ↔ ∀ (i : Fin d), -(1 / 2) * 3 ^ k < x i ∧ x i < 1 / 2 * 3 ^ k

Membership in a centered triadic cube, coordinatewise.

theorem HCPolySupport.HighContrast.Recurrence.mem_standardCell_iff {d : ℕ} {k : ℤ} {w : Fin d → ℤ} {x : Vec d} : x ∈ standardCell d k w ↔ ∀ (i : Fin d), (↑(w i) - 1 / 2) * 3 ^ k < x i ∧ x i < (↑(w i) + 1 / 2) * 3 ^ k

Membership in a standard aligned cube, coordinatewise.

theorem HCPolySupport.HighContrast.Recurrence.standardCell_eq_image {d : ℕ} (k : ℤ) (w : Fin d → ℤ) : standardCell d k w = (fun (y : Vec d) => standardCellCenter k w + y) '' centeredCube d k

A standard aligned cube is the translate of the centered cube by its own center.

Adapted cells as images

theorem HCPolySupport.HighContrast.Recurrence.adaptedCellCenter_eq {d : ℕ} (q : Mat d) (k : ℤ) (w : Fin d → ℤ) : adaptedCellCenter q k w = matVecMul q (standardCellCenter k w)

The center of an aligned adapted cell is the image of the standard center.

theorem HCPolySupport.HighContrast.Recurrence.adaptedCellAt_eq_image {d : ℕ} (q : Mat d) (k : ℤ) (w : Fin d → ℤ) : adaptedCellAt q k w = matVecMul q '' standardCell d k w

An aligned adapted cell is the grid image of a standard aligned cube.

The aligned centers inside the parent cell

theorem HCPolySupport.HighContrast.Recurrence.adaptedCellCenter_mem_adaptedCell_iff {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) {j p : ℤ} (hjp : j ≤ p) (w : Fin d → ℤ) : adaptedCellCenter q j w ∈ adaptedCell q p ↔ ∀ (i : Fin d), 2 * |w i| < 3 ^ (p - j).toNat

The index set of the aligned subdivision. For scales j ≤ p, the center 3^j q w lies in the parent cell ⋄_p^q exactly when each index w i is one of the 3^{p-j} admissible values.

Containment of the children in the parent

theorem HCPolySupport.HighContrast.Recurrence.adaptedCellAt_subset_adaptedCell {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) {j p : ℤ} (hjp : j ≤ p) {w : Fin d → ℤ} (hw : adaptedCellCenter q j w ∈ adaptedCell q p) : adaptedCellAt q j w ⊆ adaptedCell q p

Each aligned child cell lies in the parent cell. The scale ratio is odd, so the closed child cells stay inside the open parent.

Disjointness

theorem HCPolySupport.HighContrast.Recurrence.disjoint_adaptedCellAt {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (k : ℤ) {w w' : Fin d → ℤ} (hww : w ≠ w') : Disjoint (adaptedCellAt q k w) (adaptedCellAt q k w')

Distinct aligned cells at the same scale are disjoint.

The scaled adapted lattice

The count

theorem HCPolySupport.HighContrast.Recurrence.exists_finset_adaptedCellCenter_mem {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) {j p : ℤ} (hjp : j ≤ p) : ∃ (Z : Finset (Fin d → ℤ)), ↑Z = {w : Fin d → ℤ | adaptedCellCenter q j w ∈ adaptedCell q p} ∧ Z.card = 3 ^ (d * (p - j).toNat)

The aligned subdivision has 3^{d(p-j)} cells. The admissible indices form a finite set of the size prescribed by the coarse-block properties taken from HC.

theorem HCPolySupport.HighContrast.Recurrence.ncard_adaptedCellCenter_mem {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) {j p : ℤ} (hjp : j ≤ p) : {w : Fin d → ℤ | adaptedCellCenter q j w ∈ adaptedCell q p}.ncard = 3 ^ (d * (p - j).toNat)

The aligned subdivision has 3^{d(p-j)} cells. This is the counting clause of the coarse-block properties taken from HC.