High-contrast homogenization: Provider.Recurrence.AlignedSubdivision

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

The aligned subdivision of an adapted cell

The coarse-block properties taken from HC state that for a rounded grid q at alignment ℓ and integers p ≥ j ≥ ℓ the cell ⋄_p^q is partitioned by exactly 3^{d(p-j)} cells z + ⋄_j^q with z ∈ 3^j 𝕃_q ∩ ⋄_p^q, all of whose translation vectors are integral.

The adapted cubes are open, so their union omits the interior faces of the subdivision, a Lebesgue null set; the partition is a partition up to a null set, which is the form in which e.fixed.geometry.parent.child consumes it. Concretely, a point of the parent cell that misses every child cell has, in the coordinates of the grid, some coordinate exactly halfway between two consecutive multiples of 3^j, and the countably many hyperplanes carrying such points are null. Rounding each coordinate to the nearest multiple of 3^j produces the child containing the point, and the parent's own bounds place that child's index in the admissible range.

Together with the containment, disjointness, counting and integrality clauses of the companion files, this closes the aligned subdivision.

The exceptional hyperplanes

theorem HCPolySupport.HighContrast.Recurrence.volume_coord_eq {d : ℕ} (i : Fin d) (c : ℝ) : MeasureTheory.volume {x : Vec d | x i = c} = 0

A coordinate hyperplane is null.

theorem HCPolySupport.HighContrast.Recurrence.volume_gridFaces {d : ℕ} (j : ℤ) : MeasureTheory.volume (⋃ (i : Fin d), ⋃ (k : ℤ), {x : Vec d | x i = (↑k + 1 / 2) * 3 ^ j}) = 0

The grid faces at scale j — the points with some coordinate exactly halfway between two consecutive multiples of 3^j — form a null set.

Rounding a point of the parent cube to a child

theorem HCPolySupport.HighContrast.Recurrence.centeredCube_subset_iUnion_standardCell_union_gridFaces {d : ℕ} {j p : ℤ} (hjp : j ≤ p) : centeredCube d p ⊆ (⋃ w ∈ {w : Fin d → ℤ | ∀ (i : Fin d), 2 * |w i| < 3 ^ (p - j).toNat}, standardCell d j w) ∪ ⋃ (i : Fin d), ⋃ (k : ℤ), {x : Vec d | x i = (↑k + 1 / 2) * 3 ^ j}

The children cover the parent cube off the grid faces. Rounding each coordinate to the nearest multiple of 3^j lands in an admissible child unless the coordinate sits exactly on a face.

theorem HCPolySupport.HighContrast.Recurrence.volume_centeredCube_diff_iUnion_standardCell {d : ℕ} {j p : ℤ} (hjp : j ≤ p) : MeasureTheory.volume (centeredCube d p \ ⋃ w ∈ {w : Fin d → ℤ | ∀ (i : Fin d), 2 * |w i| < 3 ^ (p - j).toNat}, standardCell d j w) = 0

The children of the parent cube cover it up to a null set.

Transport to the adapted cells

theorem HCPolySupport.HighContrast.Recurrence.volume_image_matVecMul_eq_zero {d : ℕ} (q : Mat d) {s : Set (Vec d)} (hs : MeasureTheory.volume s = 0) : MeasureTheory.volume (matVecMul q '' s) = 0

The image of a null set under a grid map is null.

theorem HCPolySupport.HighContrast.Recurrence.volume_adaptedCell_diff_iUnion_adaptedCellAt {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) {j p : ℤ} (hjp : j ≤ p) : MeasureTheory.volume (adaptedCell q p \ ⋃ w ∈ {w : Fin d → ℤ | adaptedCellCenter q j w ∈ adaptedCell q p}, adaptedCellAt q j w) = 0

The aligned children cover the adapted parent cell up to a null set. This is the partition clause of the coarse-block properties taken from HC, in the form e.fixed.geometry.parent.child consumes it.

The aligned subdivision

theorem HCPolySupport.HighContrast.Recurrence.aligned_subdivision {d : ℕ} {l : ℤ} {q : Mat d} (hq : IsRoundedGrid l q) {j p : ℤ} (hlj : l ≤ j) (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) ∧ (∀ w ∈ Z, adaptedCellAt q j w ⊆ adaptedCell q p) ∧ (↑Z).PairwiseDisjoint (adaptedCellAt q j) ∧ MeasureTheory.volume (adaptedCell q p \ ⋃ w ∈ ↑Z, adaptedCellAt q j w) = 0 ∧ ∀ w ∈ Z, ∃ (v : Fin d → ℤ), adaptedCellCenter q j w = fun (i : Fin d) => ↑(v i)

The aligned subdivision of the adapted cubes. For a rounded grid at alignment ℓ and scales ℓ ≤ j ≤ p, the aligned scale-j cells whose centers lie in ⋄_p^q are contained in it, are pairwise disjoint, cover it up to a null set, number exactly 3^{d(p-j)}, and have integral translation vectors.