High-contrast homogenization: Entry.Geometry.MaximalCells

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

Maximal standard aligned cubes in a set

The family of l.source.whitney: the standard aligned cubes contained in a set W with generation at most j, and the maximal ones among them. This file has the order-theoretic part: the parent of a maximal cube of generation < j escapes W, and distinct maximal cubes are disjoint.

The definitions IsCellIn, IsMaximalCellIn, maximalCellIndices and maximalCellPairs live in the definition-only leaf HCPoly.Entry.Geometry.MaximalCellsDef (imported here), so that they can be stated without these proofs.

theorem HCPolySupport.HighContrast.Geometry.IsMaximalCellIn.le {d : ℕ} {W : Set (Vec d)} {j k : ℤ} {w : Fin d → ℤ} (h : IsMaximalCellIn W j k w) : k ≤ j

theorem HCPolySupport.HighContrast.Geometry.IsMaximalCellIn.subset {d : ℕ} {W : Set (Vec d)} {j k : ℤ} {w : Fin d → ℤ} (h : IsMaximalCellIn W j k w) : standardCell d k w ⊆ W

theorem HCPolySupport.HighContrast.Geometry.IsMaximalCellIn.parent_not_subset {d : ℕ} [NeZero d] {W : Set (Vec d)} {j k : ℤ} {w : Fin d → ℤ} (h : IsMaximalCellIn W j k w) (hkj : k < j) : ¬standardCell d (k + 1) (Transport.gridParent w) ⊆ W

The parent of a maximal cube of generation k < j is not contained in W.

theorem HCPolySupport.HighContrast.Geometry.IsMaximalCellIn.disjoint {d : ℕ} [NeZero d] {W : Set (Vec d)} {j k k' : ℤ} {w w' : Fin d → ℤ} (h : IsMaximalCellIn W j k w) (h' : IsMaximalCellIn W j k' w') (hne : (k, w) ≠ (k', w')) : Disjoint (standardCell d k w) (standardCell d k' w')

Maximal cubes with distinct index pairs are disjoint.

theorem HCPolySupport.HighContrast.Geometry.pairwiseDisjoint_maximalCellPairs {d : ℕ} [NeZero d] (W : Set (Vec d)) (j : ℤ) : (maximalCellPairs W j).PairwiseDisjoint fun (p : ℤ × (Fin d → ℤ)) => standardCell d p.1 p.2

The maximal cubes form a pairwise disjoint family indexed by their index pairs.

theorem HCPolySupport.HighContrast.Geometry.pairwiseDisjoint_maximalCellIndices {d : ℕ} [NeZero d] (W : Set (Vec d)) (j r : ℤ) : (maximalCellIndices W j r).PairwiseDisjoint fun (w : Fin d → ℤ) => standardCell d r w

The maximal cubes of one generation are pairwise disjoint.

theorem HCPolySupport.HighContrast.Geometry.isMaximalCellIn_of_greatest {d : ℕ} {W : Set (Vec d)} {j k : ℤ} {w : Fin d → ℤ} {x : Vec d} (hk : IsCellIn W j k w) (hx : x ∈ standardCell d k w) (hgreatest : ∀ (k' : ℤ) (w' : Fin d → ℤ), IsCellIn W j k' w' → x ∈ standardCell d k' w' → k' ≤ k) : IsMaximalCellIn W j k w

A cube of the family containing a point x and of largest generation among those is maximal.

theorem HCPolySupport.HighContrast.Geometry.exists_isMaximalCellIn_of_isCellIn {d : ℕ} {W : Set (Vec d)} {j k : ℤ} {w : Fin d → ℤ} {x : Vec d} (hk : IsCellIn W j k w) (hx : x ∈ standardCell d k w) : ∃ (k' : ℤ) (w' : Fin d → ℤ), IsMaximalCellIn W j k' w' ∧ x ∈ standardCell d k' w'

Every cube of the family lies in a maximal one containing any given point of it.