High-contrast homogenization: Entry.Geometry.AdaptedCellTransport

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

Transport for adapted cells

For an invertible matrix q, an adapted cell is the image of the corresponding standard cell under the linear map matVecMul q: the center of the adapted cell is the image of the standard center, and its volume is |det q| times the standard volume. Preimages along matVecMul q convert adapted cells into standard cells and back, preserving inclusion, disjointness and maximality, so that the maximal adapted cells of a set are exactly the transported maximal standard cells. These are the geometric support lemmas for the adapted Whitney partitions of l.two.grid.whitney.

theorem HCPolySupport.HighContrast.Geometry.adaptedCellAtCenter_eq_affine_standardCell {d : ℕ} (q : Mat d) (r : ℤ) (w : Fin d → ℤ) : adaptedCellAtCenter q r w = matVecMul q '' standardCell d r w

theorem HCPolySupport.HighContrast.Geometry.adaptedCellCenter_injective {d : ℕ} (q : Mat d) (r : ℤ) (hq : IsUnit q) : Function.Injective (adaptedCellCenter q r)

theorem HCPolySupport.HighContrast.Geometry.volume_adaptedCellAtCenter {d : ℕ} (q : Mat d) (r : ℤ) (w : Fin d → ℤ) : MeasureTheory.volume (adaptedCellAtCenter q r w) = ENNReal.ofReal |Matrix.det q| * ENNReal.ofReal (3 ^ r) ^ d

theorem HCPolySupport.HighContrast.Geometry.volume_adaptedCellAtCenter_ne_top {d : ℕ} (q : Mat d) (r : ℤ) (w : Fin d → ℤ) : MeasureTheory.volume (adaptedCellAtCenter q r w) ≠ ⊤

theorem HCPolySupport.HighContrast.Geometry.preimage_matVecMul_adaptedCellTranslate_eq {d : ℕ} {q q' : Mat d} (hq : IsUnit q) (j : ℤ) (y : Vec d) : matVecMul q ⁻¹' adaptedCellTranslate q' j y = adaptedCellTranslate (q⁻¹ * q') j (matVecMul q⁻¹ y)

theorem HCPolySupport.HighContrast.Geometry.preimage_matVecMul_eq_image_inv {d : ℕ} {q : Mat d} (hq : IsUnit q) (W : Set (Vec d)) : matVecMul q ⁻¹' W = matVecMul q⁻¹ '' W

theorem HCPolySupport.HighContrast.Geometry.volume_preimage_matVecMul_ne_top {d : ℕ} {q : Mat d} (hq : IsUnit q) {W : Set (Vec d)} (hW : MeasureTheory.volume W ≠ ⊤) : MeasureTheory.volume (matVecMul q ⁻¹' W) ≠ ⊤

theorem HCPolySupport.HighContrast.Geometry.IsAdaptedCellIn.to_standard_preimage {d : ℕ} {W : Set (Vec d)} {q : Mat d} {n r : ℤ} {w : Fin d → ℤ} (h : IsAdaptedCellIn W q n r w) : IsCellIn (matVecMul q ⁻¹' W) n r w

theorem HCPolySupport.HighContrast.Geometry.IsCellIn.of_standard_preimage {d : ℕ} {W : Set (Vec d)} {q : Mat d} {n r : ℤ} {w : Fin d → ℤ} (h : IsCellIn (matVecMul q ⁻¹' W) n r w) : IsAdaptedCellIn W q n r w

theorem HCPolySupport.HighContrast.Geometry.standardCell_subset_preimage_iff_adaptedCellAtCenter_subset {d : ℕ} (W : Set (Vec d)) (q : Mat d) (r : ℤ) (w : Fin d → ℤ) : standardCell d r w ⊆ matVecMul q ⁻¹' W ↔ adaptedCellAtCenter q r w ⊆ W

theorem HCPolySupport.HighContrast.Geometry.isMaximalAdaptedCellIn_iff_isMaximalCellIn_preimage {d : ℕ} (W : Set (Vec d)) (q : Mat d) (hq : IsUnit q) (n r : ℤ) (w : Fin d → ℤ) : IsMaximalAdaptedCellIn W q n r w ↔ IsMaximalCellIn (matVecMul q ⁻¹' W) n r w

theorem HCPolySupport.HighContrast.Geometry.adaptedCellAtCenter_subset_or_disjoint {d : ℕ} {q : Mat d} (hq : IsUnit q) {r r' : ℤ} (hrr' : r ≤ r') (w w' : Fin d → ℤ) : adaptedCellAtCenter q r w ⊆ adaptedCellAtCenter q r' w' ∨ Disjoint (adaptedCellAtCenter q r w) (adaptedCellAtCenter q r' w')

Aligned adapted cells in one invertible grid are nested or disjoint.

theorem HCPolySupport.HighContrast.Geometry.volume_image_iUnion_gridFaces {d : ℕ} (q : Mat d) : MeasureTheory.volume (matVecMul q '' ⋃ (k : ℤ), gridFaces d k) = 0

The affine image of all grid faces, over every integer generation, is null.