High-contrast homogenization: Entry.Geometry.AffineWhitneyCounts

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

Count-facing facts for adapted Whitney rows

Finite-level part (i) of l.two.grid.whitney: individual cell volume, top-generation packing, and lower-generation volume and cardinality estimates. The proof works in relative coordinates, using parent escape and flat-face strips. twoGridWhitneyCounts chooses one constant before all grids, scales and translations; it includes partition and finiteness, while the series identity and hybrid construction remain outside this support module.

theorem HCPolySupport.HighContrast.Geometry.adaptedCell_relVolume_le_of_gridRatio {d : ℕ} {q q' : Mat d} {K₀ : ℝ} (hd : 2 ≤ d) (hK₀ : 1 ≤ K₀) (hq : IsUnit q) (hq' : IsUnit q') (hK : gridRatio q q' ≤ K₀) (j r : ℤ) (y : Vec d) : (MeasureTheory.volume (adaptedCell q r)).toReal / (MeasureTheory.volume (adaptedCellTranslate q' j y)).toReal ≤ ↑d.factorial * K₀ ^ d * 3 ^ (-↑d * (↑j - ↑r))

theorem HCPolySupport.HighContrast.Geometry.topGenerationPacking_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 ℓ : ℤ) (hℓ : 1 ≤ ℓ) (y : Vec d) : let W := adaptedCellTranslate q' j y; have n := j - ℓ; ↑⋯.toFinset.card ≤ ↑d.factorial * K₀ ^ d * 3 ^ (↑d * ↑ℓ)

theorem HCPolySupport.HighContrast.Geometry.volume_lowerRow_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 r : ℤ) (hr : r < n) (y : Vec d) : have V := adaptedCellTranslate (q⁻¹ * q') j (matVecMul q⁻¹ y); MeasureTheory.volume (⋃ w ∈ maximalCellIndices V n r, standardCell d r w) ≤ ENNReal.ofReal (6 * ↑d * K₀ * √↑d * 3 ^ (↑r - ↑j)) * MeasureTheory.volume V

Flat-face volume bound for a capped lower row in relative coordinates. The cap is independent of the target generation; no openness of a complement is used.

theorem HCPolySupport.HighContrast.Geometry.lowerRowRelVolume_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 r : ℤ) (hr : r < n) (y : Vec d) : ∑ _z ∈ ⋯.toFinset, (MeasureTheory.volume (adaptedCell q r)).toReal / (MeasureTheory.volume (adaptedCellTranslate q' j y)).toReal ≤ 6 * ↑d * K₀ * √↑d * 3 ^ (↑r - ↑j)

The printed lower-row relative-volume estimate, for any cap n and r < n. The constant depends only on dimension and relative distortion.

theorem HCPolySupport.HighContrast.Geometry.lowerRowCard_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 r : ℤ) (hr : r < n) (y : Vec d) : ↑⋯.toFinset.card ≤ 6 * ↑d * K₀ * √↑d * (↑d.factorial * K₀ ^ d) * 3 ^ ((↑d - 1) * (↑j - ↑r))

Divide the lower-row volume bound by the positive lower cell-volume comparison.

theorem HCPolySupport.HighContrast.Geometry.twoGridWhitneyCounts (d : ℕ) (hd : 2 ≤ d) (K₀ : ℝ) (hK₀ : 1 ≤ K₀) : ∃ (C : ℝ), 0 < C ∧ ∀ (q q' : Mat d), IsUnit q → IsUnit q' → gridRatio q q' ≤ K₀ → ∀ (j ℓ : ℤ), 1 ≤ ℓ → ∀ (y : Vec d), have W := adaptedCellTranslate q' j y; ∃ (hfin : ∀ r ≤ j - ℓ, (maximalAdaptedCellCenters W q (j - ℓ) r).Finite), (∀ (r : ℤ) (w : Fin d → ℤ), IsMaximalAdaptedCellIn W q (j - ℓ) r w → adaptedCellAtCenter q r w ⊆ W) ∧ ({p : ℤ × (Fin d → ℤ) | IsMaximalAdaptedCellIn W q (j - ℓ) p.1 p.2}.PairwiseDisjoint fun (p : ℤ × (Fin d → ℤ)) => adaptedCellAtCenter q p.1 p.2) ∧ MeasureTheory.volume (W \ ⋃ p ∈ {p : ℤ × (Fin d → ℤ) | IsMaximalAdaptedCellIn W q (j - ℓ) p.1 p.2}, adaptedCellAtCenter q p.1 p.2) = 0 ∧ (∀ r ≤ j - ℓ, (MeasureTheory.volume (adaptedCell q r)).toReal / (MeasureTheory.volume W).toReal ≤ C * 3 ^ (-↑d * (↑j - ↑r))) ∧ ↑⋯.toFinset.card ≤ C * 3 ^ (↑d * ↑ℓ) ∧ (∀ (r : ℤ) (hr : r < j - ℓ), ↑⋯.toFinset.card ≤ C * 3 ^ ((↑d - 1) * (↑j - ↑r))) ∧ ∀ (r : ℤ) (hr : r < j - ℓ), ∑ _z ∈ ⋯.toFinset, (MeasureTheory.volume (adaptedCell q r)).toReal / (MeasureTheory.volume W).toReal ≤ C * 3 ^ (↑r - ↑j)

Finite-level part (i) of l.two.grid.whitney. One constant is chosen before all grids, scales and translations. Null exhaustion is included; the infinite-series identity and the hybrid construction are separate tasks.