High-contrast homogenization: Entry.Geometry.HybridWhitneyUncovered

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

Hybrid Whitney Uncovered

The faces and the boundary layer of the hybrid Whitney decomposition, and the measure of the part of the domain they leave uncovered. The packed adapted cells, their exposed faces and the affine neighborhoods of uncovered points are bounded at the cap scale, the uncovered part lies in the outer strip modulo the null new-grid faces, and in its own coordinates the packed union is exactly a union of standard cells. This serves l.two.grid.whitney.

Packed adapted cells and the null grid seams

EccentricityScaleDecay for construction (ii) of l.two.grid.whitney. The uncovered set includes internal open-cell seams. Off the new-grid faces its points are interior points; all pointwise boundary arguments must retain this null exception. No replacement of the uncovered set is made.

theorem HCPolySupport.HighContrast.Geometry.contained_adaptedCellIndices_eq_cap {d : ℕ} [NeZero d] {q : Mat d} (hq : IsUnit q) (W : Set (Vec d)) (n : ℤ) : {w : Fin d → ℤ | adaptedCellAtCenter q n w ⊆ W} = maximalAdaptedCellIndices W q n n

The packed index family is the cap row of the actual maximal family.

theorem HCPolySupport.HighContrast.Geometry.finite_contained_adaptedCellIndices {d : ℕ} [NeZero d] {q : Mat d} (hq : IsUnit q) {W : Set (Vec d)} (hW : MeasureTheory.volume W ≠ ⊤) (n : ℤ) : {w : Fin d → ℤ | adaptedCellAtCenter q n w ⊆ W}.Finite

Positive-volume disjoint cap cells form a finite family inside finite volume.

theorem HCPolySupport.HighContrast.Geometry.adaptedCellAtCenter_disjoint_of_ne {d : ℕ} {q : Mat d} (hq : IsUnit q) (n : ℤ) {w v : Fin d → ℤ} (hwv : w ≠ v) : Disjoint (adaptedCellAtCenter q n w) (adaptedCellAtCenter q n v)

Distinct indices in an invertible grid give disjoint open cells.

theorem HCPolySupport.HighContrast.Geometry.isMaximalAdaptedCellIn_interior_iff {d : ℕ} {q : Mat d} (hq : IsUnit q) (W : Set (Vec d)) (n r : ℤ) (w : Fin d → ℤ) : IsMaximalAdaptedCellIn (interior W) q n r w ↔ IsMaximalAdaptedCellIn W q n r w

An open adapted cell is contained in a set exactly when it is contained in its interior; consequently the maximal predicate is unchanged.

theorem HCPolySupport.HighContrast.Geometry.exists_mem_adaptedCellAtCenter_of_not_mem_gridFaces {d : ℕ} {q : Mat d} (hq : IsUnit q) (n : ℤ) {x : Vec d} (hx : x ∉ matVecMul q '' gridFaces d n) : ∃ (w : Fin d → ℤ), x ∈ adaptedCellAtCenter q n w

Outside the affine generation faces there is an actual open adapted cell.

theorem HCPolySupport.HighContrast.Geometry.adaptedCellAtCenter_disjoint_adaptedCoveredPart {d : ℕ} {q : Mat d} (hq : IsUnit q) (W : Set (Vec d)) (n : ℤ) (w : Fin d → ℤ) (hw : ¬adaptedCellAtCenter q n w ⊆ W) : Disjoint (adaptedCellAtCenter q n w) (adaptedCoveredPart W q n)

An unpacked cell cannot meet any cell in the packed generation.

theorem HCPolySupport.HighContrast.Geometry.adaptedUncoveredPart_diff_interior_subset_gridFaces {d : ℕ} {q : Mat d} (hq : IsUnit q) {W : Set (Vec d)} (hW : IsOpen W) (n : ℤ) : adaptedUncoveredPart W q n \ interior (adaptedUncoveredPart W q n) ⊆ matVecMul q '' gridFaces d n

Internal packed seams can remain uncovered, but away from the new-grid faces every uncovered point is interior. This is the a.e. reading required by the strip argument in l.two.grid.whitney.

theorem HCPolySupport.HighContrast.Geometry.volume_adaptedUncoveredPart_diff_interior {d : ℕ} {q : Mat d} (hq : IsUnit q) {W : Set (Vec d)} (hW : IsOpen W) (n : ℤ) : MeasureTheory.volume (adaptedUncoveredPart W q n \ interior (adaptedUncoveredPart W q n)) = 0

The interior exhausts the uncovered part modulo new-grid faces.

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

The packed family and the actual maximal old cells exhaust an open parent. The uncovered set itself need not be open. This includes the empty packed family.

theorem HCPolySupport.HighContrast.Geometry.sum_sq_sub_le_of_mem_neighbor_standardCells {d : ℕ} {n : ℤ} {w v : Fin d → ℤ} (hwv : ∀ (i : Fin d), |↑(w i) - ↑(v i)| ≤ 1) {x y : Vec d} (hx : x ∈ standardCell d n w) (hy : y ∈ standardCell d n v) : ∑ i : Fin d, (x i - y i) ^ 2 ≤ (2 * √↑d * 3 ^ n) ^ 2

Points in lattice-neighbor cells are at distance at most twice the usual cell diameter. The hypothesis also allows diagonal neighbors.

theorem HCPolySupport.HighContrast.Geometry.volume_exposed_adaptedCells_preimage_le_of_gridRatio {d : ℕ} [NeZero d] {q q' : Mat d} {K₀ : ℝ} (hd : 2 ≤ d) (hK₀ : 1 ≤ K₀) (hq : IsUnit q) (hq' : IsUnit q') (hK : gridRatio q q' ≤ K₀) (j n : ℤ) (y : Vec d) : have W := adaptedCellTranslate q j y; have E := {w : Fin d → ℤ | adaptedCellAtCenter q' n w ⊆ W ∧ ∃ (i : Fin d) (b : Bool), ¬adaptedCellAtCenter q' n (Function.update w i (w i + if b = true then 1 else -1)) ⊆ W}; MeasureTheory.volume (⋃ w ∈ E, standardCell d n w) ≤ ENNReal.ofReal (4 * ↑d * K₀ * √↑d * 3 ^ (↑n - ↑j)) * MeasureTheory.volume (matVecMul q' ⁻¹' W)

A packed face is exposed when its lattice neighbor across that face is unpacked. Only cubes with such a face enter this union; interior packed seams contribute nothing to the estimate.

theorem HCPolySupport.HighContrast.Geometry.ncard_exposed_adaptedCells_le_of_gridRatio {d : ℕ} [NeZero d] {q q' : Mat d} {K₀ : ℝ} (hd : 2 ≤ d) (hK₀ : 1 ≤ K₀) (hq : IsUnit q) (hq' : IsUnit q') (hK : gridRatio q q' ≤ K₀) (j n : ℤ) (y : Vec d) : have W := adaptedCellTranslate q j y; have E := {w : Fin d → ℤ | adaptedCellAtCenter q' n w ⊆ W ∧ ∃ (i : Fin d) (b : Bool), ¬adaptedCellAtCenter q' n (Function.update w i (w i + if b = true then 1 else -1)) ⊆ W}; ↑E.ncard ≤ 4 * ↑d * K₀ * √↑d * (↑d.factorial * K₀ ^ d) * 3 ^ ((↑d - 1) * (↑j - ↑n))

There are at most C(d,K₀) 3^((d-1)(j-n)) packed cubes with exposed faces. The cap family is proved finite inside this theorem.

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

In its own invertible grid coordinates the packed union is exactly the packed union of standard cells.

The outer strip of the hybrid Whitney construction

The uncovered part of l.two.grid.whitney lies in the outer strip modulo the explicitly excluded new-grid faces. All metric estimates use relative coordinates; neither absolute matrix norm is bounded.

theorem HCPolySupport.HighContrast.Geometry.exists_not_mem_of_mem_uncovered_preimage {d : ℕ} (q : Mat d) (W : Set (Vec d)) (n : ℤ) {x : Vec d} (hx : matVecMul q x ∈ adaptedUncoveredPart W q n) (hxN : x ∉ gridFaces d n) : ∃ x' ∉ matVecMul q ⁻¹' W, ∑ i : Fin d, (x i - x' i) ^ 2 ≤ (√↑d * 3 ^ n) ^ 2

In the packed grid's coordinates an uncovered point off grid faces shares a generation-n cell with a point outside the parent.

theorem HCPolySupport.HighContrast.Geometry.volume_adaptedUncoveredPart_le_of_gridRatio {d : ℕ} [NeZero d] {q q' : Mat d} {K₀ : ℝ} (hd : 2 ≤ d) (hK₀ : 1 ≤ K₀) (hq : IsUnit q) (hq' : IsUnit q') (hK : gridRatio q q' ≤ K₀) (j n : ℤ) (y : Vec d) : MeasureTheory.volume (adaptedUncoveredPart (adaptedCellTranslate q j y) q' n) ≤ ENNReal.ofReal (2 * ↑d * K₀ * √↑d * 3 ^ (↑n - ↑j)) * MeasureTheory.volume (adaptedCellTranslate q j y)

The whole uncovered volume satisfies the cap-scale outer-strip estimate. The proof removes the new-grid faces before applying the pointwise strip lemma, then restores them using their zero measure.

theorem HCPolySupport.HighContrast.Geometry.volume_standard_face_neighborhood {d : ℕ} (n : ℤ) (w : Fin d → ℤ) (i : Fin d) (b : Bool) (t : ℝ) : have a := (↑(w i) + if b = true then 1 / 2 else -1 / 2) * 3 ^ n; MeasureTheory.volume (Set.univ.pi (Function.update (fun (k : Fin d) => Set.Icc ((↑(w k) - 1 / 2) * 3 ^ n - t) ((↑(w k) + 1 / 2) * 3 ^ n + t)) i (Set.Icc (a - t) (a + t)))) = ENNReal.ofReal (2 * t) * ENNReal.ofReal (3 ^ n + 2 * t) ^ (d - 1)

Exact volume of a width-t rectangular neighborhood of a packed face. The other coordinates are enlarged by t, so this includes its end caps.

theorem HCPolySupport.HighContrast.Geometry.volume_standard_face_neighborhood_le {d : ℕ} (n r : ℤ) (hr : r ≤ n) (w : Fin d → ℤ) (i : Fin d) (b : Bool) {c : ℝ} (hc : 0 ≤ c) : have t := c * 3 ^ r; have a := (↑(w i) + if b = true then 1 / 2 else -1 / 2) * 3 ^ n; MeasureTheory.volume (Set.univ.pi (Function.update (fun (k : Fin d) => Set.Icc ((↑(w k) - 1 / 2) * 3 ^ n - t) ((↑(w k) + 1 / 2) * 3 ^ n + t)) i (Set.Icc (a - t) (a + t)))) ≤ ENNReal.ofReal (2 * c * (1 + 2 * c) ^ (d - 1) * 3 ^ r * (3 ^ n) ^ (d - 1))

At r ≤ n the end-cap contribution is absorbed into a constant independent of both generations; the coefficient may depend on the width multiplier c, as required after relative matrix distortion.

theorem HCPolySupport.HighContrast.Geometry.exposed_face_near_uncovered_point {d : ℕ} [NeZero d] (W : Set (Vec d)) (hW : MeasureTheory.volume W ≠ ⊤) (n : ℤ) (x y : Vec d) (hxN : x ∉ gridFaces d n) (hx : x ∉ adaptedCoveredPart W 1 n) (hy : y ∈ adaptedCoveredPart W 1 n) (s : ℝ) (hs : 0 ≤ s) (hxy : ∀ (k : Fin d), |x k - y k| ≤ s) : ∃ (w : Fin d → ℤ), adaptedCellAtCenter 1 n w ⊆ W ∧ ∃ (i : Fin d) (b : Bool), ¬adaptedCellAtCenter 1 n (Function.update w i (w i + if b = true then 1 else -1)) ⊆ W ∧ have t := ↑d * s; have a := (↑(w i) + if b = true then 1 / 2 else -1 / 2) * 3 ^ n; x ∈ Set.univ.pi (Function.update (fun (k : Fin d) => Set.Icc ((↑(w k) - 1 / 2) * 3 ^ n - t) ((↑(w k) + 1 / 2) * 3 ^ n + t)) i (Set.Icc (a - t) (a + t)))

A finite closest-cell argument finds an exposed packed face near an uncovered point whenever a packed point is nearby. Internal packed seams are excluded by the explicit generation-face hypothesis.

theorem HCPolySupport.HighContrast.Geometry.volume_iUnion_affine_face_neighborhoods_le {d : ℕ} (P : Mat d) (F : Finset (Fin d → ℤ)) (n r : ℤ) (hr : r ≤ n) {c : ℝ} (hc : 0 ≤ c) : have t := c * 3 ^ r; have B := fun (w : Fin d → ℤ) (i : Fin d) (b : Bool) => have a := (↑(w i) + if b = true then 1 / 2 else -1 / 2) * 3 ^ n; Set.univ.pi (Function.update (fun (k : Fin d) => Set.Icc ((↑(w k) - 1 / 2) * 3 ^ n - t) ((↑(w k) + 1 / 2) * 3 ^ n + t)) i (Set.Icc (a - t) (a + t))); MeasureTheory.volume (⋃ w ∈ F, ⋃ (i : Fin d), ⋃ (b : Bool), matVecMul P '' B w i b) ≤ ENNReal.ofReal (↑F.card * (2 * ↑d) * |Matrix.det P| * (2 * c * (1 + 2 * c) ^ (d - 1)) * 3 ^ r * (3 ^ n) ^ (d - 1))

The affine neighborhoods of all faces in a finite cube family have the expected width times surface-volume bound, including overlaps and end caps.