High-contrast homogenization: Entry.Geometry.TwoGridWhitney

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

Countable volume assembly for the actual adapted Whitney rows

The rows are indexed by the entire admissible integer subtype and their finite center sets. Summability is proved from finite measure before the real series is evaluated, as required by l.two.grid.whitney.

theorem HCPolySupport.HighContrast.Geometry.volume_maximalAdaptedCell_row_toReal {d : ℕ} [NeZero d] {q : Mat d} (hq : IsUnit q) (W : Set (Vec d)) (n r : ℤ) (hfin : (maximalAdaptedCellCenters W q n r).Finite) : (MeasureTheory.volume (⋃ w ∈ maximalAdaptedCellIndices W q n r, adaptedCellAtCenter q r w)).toReal = ∑ _z ∈ hfin.toFinset, (MeasureTheory.volume (adaptedCell q r)).toReal

Center injectivity converts a disjoint index-row volume to the finite center sum, for any witness of its finiteness.

theorem HCPolySupport.HighContrast.Geometry.hasSum_maximalAdaptedCell_row_volumes {d : ℕ} [NeZero d] {q : Mat d} (hq : IsUnit q) {W : Set (Vec d)} (hW : MeasureTheory.volume W ≠ ⊤) (n : ℤ) (hfin : ∀ r ≤ n, (maximalAdaptedCellCenters W q n r).Finite) : HasSum (fun (r : { r : ℤ // r ≤ n }) => ∑ _z ∈ ⋯.toFinset, (MeasureTheory.volume (adaptedCell q ↑r)).toReal) (MeasureTheory.volume (⋃ p ∈ {p : ℤ × (Fin d → ℤ) | IsMaximalAdaptedCellIn W q n p.1 p.2}, adaptedCellAtCenter q p.1 p.2)).toReal

The full admissible integer family is summable, with sum equal to the measure of its actual pair-indexed union. Finite measure is used before passing from the extended nonnegative series to a real series.

theorem HCPolySupport.HighContrast.Geometry.hasSum_maximalAdaptedCell_relVolumes {d : ℕ} [NeZero d] {q : Mat d} (hq : IsUnit q) {W : Set (Vec d)} (hWopen : IsOpen W) (hW0 : MeasureTheory.volume W ≠ 0) (hW : MeasureTheory.volume W ≠ ⊤) (n : ℤ) (hfin : ∀ r ≤ n, (maximalAdaptedCellCenters W q n r).Finite) : HasSum (fun (r : { r : ℤ // r ≤ n }) => ∑ _z ∈ ⋯.toFinset, (MeasureTheory.volume (adaptedCell q ↑r)).toReal / (MeasureTheory.volume W).toReal) 1

Every finite-volume open target of positive volume has total normalized Whitney mass one, with genuine summability on the infinite lower half-line.

theorem HCPolySupport.HighContrast.Geometry.maximalAdaptedCell_row_relVolume_le {d : ℕ} [NeZero d] {q : Mat d} (hq : IsUnit q) (W : Set (Vec d)) (n r : ℤ) (hfin : (maximalAdaptedCellCenters W q n r).Finite) {V : Set (Vec d)} (hV0 : MeasureTheory.volume V ≠ 0) (hV : MeasureTheory.volume V ≠ ⊤) {C : ℝ} (hC : 0 ≤ C) (hle : MeasureTheory.volume (⋃ w ∈ maximalAdaptedCellIndices W q n r, adaptedCellAtCenter q r w) ≤ ENNReal.ofReal C * MeasureTheory.volume V) : ∑ _z ∈ hfin.toFinset, (MeasureTheory.volume (adaptedCell q r)).toReal / (MeasureTheory.volume V).toReal ≤ C

A measure bound for an actual adapted row gives the normalized center sum, with a separately specified positive finite denominator.

theorem HCPolySupport.HighContrast.Geometry.two_grid_whitney_part_one (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 : { r : ℤ // r ≤ j - ℓ }), ∑ _z ∈ ⋯.toFinset, (MeasureTheory.volume (adaptedCell q ↑r)).toReal / (MeasureTheory.volume W).toReal = 1 ∧ ∀ (r : ℤ) (hr : r < j - ℓ), ∑ _z ∈ ⋯.toFinset, (MeasureTheory.volume (adaptedCell q r)).toReal / (MeasureTheory.volume W).toReal ≤ C * 3 ^ (↑r - ↑j)

Complete construction (i), including the infinite real-series identity. The same positive constant is chosen before every grid, scale and translation.

theorem HCPolySupport.HighContrast.Geometry.hybrid_whitney_partition_cap {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 U := adaptedUncoveredPart W q' n; ∃ (hfin : ∀ r ≤ n, (maximalAdaptedCellCenters U q n r).Finite), (∀ (r : ℤ) (w : Fin d → ℤ), IsMaximalAdaptedCellIn U q n r w → adaptedCellAtCenter q r w ⊆ U) ∧ ({p : ℤ × (Fin d → ℤ) | IsMaximalAdaptedCellIn U q n p.1 p.2}.PairwiseDisjoint fun (p : ℤ × (Fin d → ℤ)) => adaptedCellAtCenter q p.1 p.2) ∧ MeasureTheory.volume (W \ (adaptedCoveredPart W q' n ∪ ⋃ p ∈ {p : ℤ × (Fin d → ℤ) | IsMaximalAdaptedCellIn U q n p.1 p.2}, adaptedCellAtCenter q p.1 p.2)) = 0 ∧ ∑ _z ∈ ⋯.toFinset, (MeasureTheory.volume (adaptedCell q n)).toReal / (MeasureTheory.volume W).toReal ≤ 2 * ↑d * K₀ * √↑d * 3 ^ (↑n - ↑j)

The hybrid construction's finiteness, exact null partition, and cap-row estimate. The smaller-row exposed-face estimate is a separate obligation.

theorem HCPolySupport.HighContrast.Geometry.hybrid_lower_row_subset_boundary_neighborhoods {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 W := adaptedCellTranslate q j y; have U := adaptedUncoveredPart W q' n; have P := q⁻¹ * q'; have c := 3 * ↑d * K₀ * √↑d; have t := c * 3 ^ r; 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}; 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))); (⋃ w ∈ maximalAdaptedCellIndices U q n r, standardCell d r w) \ matVecMul P '' gridFaces d n ⊆ (fun (v : Vec d) => matVecMul q⁻¹ y + matVecMul 1 v) '' boundaryStrips d j (√↑d * 3 ^ (r + 1)) ∪ ⋃ w ∈ E, ⋃ (i : Fin d), ⋃ (b : Bool), matVecMul P '' B w i b

Every smaller selected old cube lies, away from the specified null new-grid faces, near the outer boundary or an exposed packed face. Both relative matrices are retained throughout the coordinate transport.

theorem HCPolySupport.HighContrast.Geometry.volume_hybrid_lower_row_le (d : ℕ) (hd : 2 ≤ d) (K₀ : ℝ) (hK₀ : 1 ≤ K₀) : ∃ (C : ℝ), 0 < C ∧ ∀ (q q' : Mat d), IsUnit q → IsUnit q' → gridRatio q q' ≤ K₀ → ∀ (j n r : ℤ), r < n → ∀ (y : Vec d), MeasureTheory.volume (⋃ w ∈ maximalAdaptedCellIndices (adaptedUncoveredPart (adaptedCellTranslate q j y) q' n) q n r, standardCell d r w) ≤ ENNReal.ofReal (C * 3 ^ r * (3 ^ j) ^ (d - 1))

The smaller hybrid row has width times surface-volume mass in old-grid coordinates. The constant is chosen before both matrices and all scales.

theorem HCPolySupport.HighContrast.Geometry.hybrid_lower_row_relVolume_bounds (d : ℕ) (hd : 2 ≤ d) (K₀ : ℝ) (hK₀ : 1 ≤ K₀) : ∃ (C : ℝ), 0 < C ∧ ∀ (q q' : Mat d), IsUnit q → IsUnit q' → gridRatio q q' ≤ K₀ → ∀ (j n r : ℤ), r < n → ∀ (y : Vec d), have W := adaptedCellTranslate q j y; have U := adaptedUncoveredPart W q' n; ∃ (hfin : (maximalAdaptedCellCenters U q n r).Finite), ∑ _z ∈ hfin.toFinset, (MeasureTheory.volume (adaptedCell q r)).toReal / (MeasureTheory.volume W).toReal ≤ C * 3 ^ (↑r - ↑j)

The smaller hybrid rows satisfy the required 3^(r-j) relative-volume bound, with finiteness produced and one constant before all other data.

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

Complete construction (ii), including the cap and every smaller row. Neither openness nor finiteness of the uncovered set is an extra premise.