High-contrast homogenization: Provider.Transport.WhitneyCells

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

Nesting of the aligned cells of one grid

The maximal filling of l.two.grid.whitney is run in the coordinates of the grid it selects from, where the adapted cells of a rounded geometry become the standard aligned triadic cubes: in their half-open realizations these tile ℝ^d exactly, and any two of them, of any two scales, are nested or disjoint.

This file records that tiling for the open realizations the formalization uses. The aligned parent of the scale-a index w is the scale-a+1 index ⌊(w+1)/3⌋, coordinatewise; a cell is contained in its parent, hence in each of its iterated ancestors; two cells of any two scales that share a point are nested, because the finer one lies in an ancestor of its own scale and distinct cells of one scale are disjoint; and every point off the countable family of grid faces lies in a cell of each scale, the face family being the null set the covering statements discard.

The aligned parent

def HCPolySupport.HighContrast.Transport.gridParent {d : ℕ} (w : Fin d → ℤ) : Fin d → ℤ

The aligned parent index. The scale-a cell of index w sits inside the scale-a+1 cell of index gridParent w, coordinatewise ⌊(w+1)/3⌋; this is the "aligned u-parent of scale a+1" of the selection rule of l.two.grid.whitney(i).

Equations

• HCPolySupport.HighContrast.Transport.gridParent w i = (w i + 1) / 3

theorem HCPolySupport.HighContrast.Transport.standardCell_subset_parent {d : ℕ} (a : ℤ) (w : Fin d → ℤ) : standardCell d a w ⊆ standardCell d (a + 1) (gridParent w)

A standard aligned cube lies in its aligned parent. The parent index is ⌊(w+1)/3⌋ coordinatewise, the unique scale-a+1 index whose cube contains the scale-a cube of index w.

theorem HCPolySupport.HighContrast.Transport.adaptedCellAt_subset_parent {d : ℕ} (q : Mat d) (a : ℤ) (w : Fin d → ℤ) : adaptedCellAt q a w ⊆ adaptedCellAt q (a + 1) (gridParent w)

An aligned adapted cell lies in its aligned parent.

theorem HCPolySupport.HighContrast.Transport.adaptedCellAt_subset_ancestor {d : ℕ} (q : Mat d) (a : ℤ) (w : Fin d → ℤ) (k : ℕ) : adaptedCellAt q a w ⊆ adaptedCellAt q (a + ↑k) (gridParent^[k] w)

An aligned adapted cell lies in each of its iterated ancestors.

Two cells of any two scales are nested or disjoint

theorem HCPolySupport.HighContrast.Transport.adaptedCellAt_subset_of_mem_of_mem {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) {a b : ℤ} (hab : a ≤ b) {w v : Fin d → ℤ} {x : Vec d} (hxw : x ∈ adaptedCellAt q a w) (hxv : x ∈ adaptedCellAt q b v) : adaptedCellAt q a w ⊆ adaptedCellAt q b v

Cells of two scales that share a point are nested. The finer cell lies in its own ancestor at the coarser scale, and distinct cells of one scale are disjoint, so that ancestor is the coarser cell.

Every point off the grid faces lies in a cell

theorem HCPolySupport.HighContrast.Transport.exists_mem_standardCell {d : ℕ} {a : ℤ} {x : Vec d} (hx : ∀ (i : Fin d) (k : ℤ), x i ≠ (↑k + 1 / 2) * 3 ^ a) : ∃ (w : Fin d → ℤ), x ∈ standardCell d a w

The standard aligned cubes of one scale cover their complement of the grid faces. Rounding each coordinate to the nearest multiple of 3^a produces the cube containing the point, unless the coordinate sits exactly on a face.

theorem HCPolySupport.HighContrast.Transport.volume_image_gridFaces {d : ℕ} (q : Mat d) (a : ℤ) : MeasureTheory.volume (matVecMul q '' ⋃ (i : Fin d), ⋃ (k : ℤ), {z : Vec d | z i = (↑k + 1 / 2) * 3 ^ a}) = 0

The grid faces of one scale, carried to the grid of q, form a null set.

theorem HCPolySupport.HighContrast.Transport.exists_mem_adaptedCellAt {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (a : ℤ) {x : Vec d} (hx : x ∉ matVecMul q '' ⋃ (i : Fin d), ⋃ (k : ℤ), {z : Vec d | z i = (↑k + 1 / 2) * 3 ^ a}) : ∃ (w : Fin d → ℤ), x ∈ adaptedCellAt q a w

The aligned cells of one scale cover the complement of the grid faces.