High-contrast homogenization: Entry.Geometry.AdaptedMaximalCells

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

Maximal adapted cells

Order-theoretic facts for the actual adapted maximal-cell predicate, transported from the standard maximal-cell family through an invertible adapted grid: the maximal adapted cells are pairwise disjoint, their index set is the maximal standard-cell index set of the affine preimage, their center set is finite when the region has finite volume, and the part of an open region missed by the maximal cells off the affine grid faces is null. These are the cell-ordering and covering facts behind the Whitney partition between adapted grids l.two.grid.whitney, and they also supply the capped adapted covering used by p.response.transfer.

theorem HCPolySupport.HighContrast.Geometry.IsMaximalAdaptedCellIn.subset {d : ℕ} {W : Set (Vec d)} {q : Mat d} {n r : ℤ} {w : Fin d → ℤ} (h : IsMaximalAdaptedCellIn W q n r w) : adaptedCellAtCenter q r w ⊆ W

theorem HCPolySupport.HighContrast.Geometry.matVecMul_injective_of_isUnit {d : ℕ} (q : Mat d) (hq : IsUnit q) : Function.Injective (matVecMul q)

theorem HCPolySupport.HighContrast.Geometry.IsMaximalAdaptedCellIn.disjoint {d : ℕ} [NeZero d] {W : Set (Vec d)} {q : Mat d} (hq : IsUnit q) {n r r' : ℤ} {w w' : Fin d → ℤ} (h : IsMaximalAdaptedCellIn W q n r w) (h' : IsMaximalAdaptedCellIn W q n r' w') (hne : (r, w) ≠ (r', w')) : Disjoint (adaptedCellAtCenter q r w) (adaptedCellAtCenter q r' w')

theorem HCPolySupport.HighContrast.Geometry.pairwiseDisjoint_maximalAdaptedCellPairs {d : ℕ} [NeZero d] (W : Set (Vec d)) (q : Mat d) (hq : IsUnit q) (n : ℤ) : {p : ℤ × (Fin d → ℤ) | IsMaximalAdaptedCellIn W q n p.1 p.2}.PairwiseDisjoint fun (p : ℤ × (Fin d → ℤ)) => adaptedCellAtCenter q p.1 p.2

theorem HCPolySupport.HighContrast.Geometry.pairwiseDisjoint_maximalAdaptedCellIndices {d : ℕ} [NeZero d] (W : Set (Vec d)) (q : Mat d) (hq : IsUnit q) (n r : ℤ) : (maximalAdaptedCellIndices W q n r).PairwiseDisjoint fun (w : Fin d → ℤ) => adaptedCellAtCenter q r w

theorem HCPolySupport.HighContrast.Geometry.isMaximalCellIn_iff_parent_not_subset {d : ℕ} [NeZero d] {W : Set (Vec d)} (n r : ℤ) (w : Fin d → ℤ) : IsMaximalCellIn W n r w ↔ r ≤ n ∧ standardCell d r w ⊆ W ∧ (r = n ∨ ¬standardCell d (r + 1) (Transport.gridParent w) ⊆ W)

theorem HCPolySupport.HighContrast.Geometry.isMaximalAdaptedCellIn_iff_parent_not_subset {d : ℕ} [NeZero d] {W : Set (Vec d)} {q : Mat d} (hq : IsUnit q) (n r : ℤ) (w : Fin d → ℤ) : IsMaximalAdaptedCellIn W q n r w ↔ r ≤ n ∧ adaptedCellAtCenter q r w ⊆ W ∧ (r = n ∨ ¬adaptedCellAtCenter q (r + 1) (Transport.gridParent w) ⊆ W)

theorem HCPolySupport.HighContrast.Geometry.exists_isAdaptedCellIn_of_isOpen {d : ℕ} {W : Set (Vec d)} {q : Mat d} (hq : IsUnit q) (hW : IsOpen W) (n : ℤ) {x : Vec d} (hxW : x ∈ W) (hxN : x ∉ matVecMul q '' ⋃ (k : ℤ), gridFaces d k) : ∃ (r : ℤ) (w : Fin d → ℤ), IsAdaptedCellIn W q n r w ∧ x ∈ adaptedCellAtCenter q r w

An interior point off all affine grid faces has a contained cell below any prescribed cap. Smallness is measured with the ambient sup metric.

theorem HCPolySupport.HighContrast.Geometry.exists_isMaximalAdaptedCellIn_of_isAdaptedCellIn {d : ℕ} {W : Set (Vec d)} {q : Mat d} (hq : IsUnit q) {n r : ℤ} {w : Fin d → ℤ} {x : Vec d} (hw : IsAdaptedCellIn W q n r w) (hx : x ∈ adaptedCellAtCenter q r w) : ∃ (r' : ℤ) (w' : Fin d → ℤ), IsMaximalAdaptedCellIn W q n r' w' ∧ x ∈ adaptedCellAtCenter q r' w'

Lift a contained adapted cell through standard maximal existence at the same cap.

theorem HCPolySupport.HighContrast.Geometry.volume_diff_iUnion_maximalAdaptedCells_of_isOpen {d : ℕ} {W : Set (Vec d)} {q : Mat d} (hq : IsUnit q) (hW : IsOpen W) (n : ℤ) : MeasureTheory.volume (W \ ⋃ p ∈ {p : ℤ × (Fin d → ℤ) | IsMaximalAdaptedCellIn W q n p.1 p.2}, adaptedCellAtCenter q p.1 p.2) = 0

theorem HCPolySupport.HighContrast.Geometry.finite_maximalAdaptedCellCenters_of_finite_indices {d : ℕ} {W : Set (Vec d)} {q : Mat d} {n r : ℤ} (hfin : (maximalAdaptedCellIndices W q n r).Finite) : (maximalAdaptedCellCenters W q n r).Finite

theorem HCPolySupport.HighContrast.Geometry.maximalAdaptedCellCenters_eq_image_indices {d : ℕ} (W : Set (Vec d)) (q : Mat d) (n r : ℤ) : maximalAdaptedCellCenters W q n r = adaptedCellCenter q r '' maximalAdaptedCellIndices W q n r

theorem HCPolySupport.HighContrast.Geometry.maximalAdaptedCellIndices_eq_maximalCellIndices_preimage {d : ℕ} (W : Set (Vec d)) (q : Mat d) (hq : IsUnit q) (n r : ℤ) : maximalAdaptedCellIndices W q n r = maximalCellIndices (matVecMul q ⁻¹' W) n r

theorem HCPolySupport.HighContrast.Geometry.finite_maximalAdaptedCellIndices_of_volume_ne_top {d : ℕ} [NeZero d] {W : Set (Vec d)} {q : Mat d} (hq : IsUnit q) (hW : MeasureTheory.volume W ≠ ⊤) (n r : ℤ) : (maximalAdaptedCellIndices W q n r).Finite

theorem HCPolySupport.HighContrast.Geometry.finite_maximalAdaptedCellCenters_of_volume_ne_top {d : ℕ} [NeZero d] {W : Set (Vec d)} {q : Mat d} (hq : IsUnit q) (hW : MeasureTheory.volume W ≠ ⊤) (n r : ℤ) : (maximalAdaptedCellCenters W q n r).Finite

theorem HCPolySupport.HighContrast.Geometry.ncard_maximalAdaptedCellCenters_eq_preimage {d : ℕ} {W : Set (Vec d)} {q : Mat d} (hq : IsUnit q) (n r : ℤ) : (maximalAdaptedCellCenters W q n r).ncard = (maximalCellIndices (matVecMul q ⁻¹' W) n r).ncard

The actual center row and its standard preimage row have the same cardinality.

theorem HCPolySupport.HighContrast.Geometry.exists_not_mem_preimage_of_mem_maximalAdaptedCell {d : ℕ} [NeZero d] {W : Set (Vec d)} {q : Mat d} (hq : IsUnit q) {n r : ℤ} (hr : r < n) {w : Fin d → ℤ} (hw : IsMaximalAdaptedCellIn W q n r w) {x : Vec d} (hx : x ∈ standardCell d r w) : ∃ x' ∉ matVecMul q ⁻¹' W, ∑ i : Fin d, (x i - x' i) ^ 2 ≤ (√↑d * 3 ^ (r + 1)) ^ 2

Below the cap, parent escape controls distance to the complement in q-coordinates.