High-contrast homogenization: Provider.PolynomialHomogenization.ConvexWhitneyGeometry

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

Euclidean Whitney rows in bounded domains

The identity-grid maximal filling gives finite rows of ordinary open triadic cubes. Its selected cubes are disjoint, lie inside the target, have escaping parents below the starting scale, and exhaust every bounded open target up to a null set. For convex targets, the escaping-parent property and the inner ball bound the volume of each row.

theorem HCPolySupport.HighContrast.adaptedCellAt_one_eq_openCubeSet_translateCube {d : ℕ} (a : ℤ) (w : Fin d → ℤ) : adaptedCellAt 1 a w = openCubeSet (translateCube w (originCube d a))

An aligned cell of the identity grid is exactly the corresponding open translated triadic cube.

theorem HCPolySupport.HighContrast.fillingIndex_one_cell_and_parent_escape {d : ℕ} {U : Set (Vec d)} {n a : ℤ} (han : a < n) {w : Fin d → ℤ} (hw : w ∈ Transport.fillingIndex 1 n U a) : openCubeSet (translateCube w (originCube d a)) ⊆ U ∧ ¬openCubeSet (translateCube (Transport.gridParent w) (originCube d (a + 1))) ⊆ U

A selected identity-grid cube lies in the target, while below the starting scale its aligned parent escapes the target.

theorem HCPolySupport.HighContrast.iUnion_fillingIndex_one_subset_innerBoundaryLayer {d : ℕ} (hd : 1 ≤ d) {U : Set (Vec d)} {n a : ℤ} (han : a < n) : ⋃ w ∈ Transport.fillingIndex 1 n U a, openCubeSet (translateCube w (originCube d a)) ⊆ {x : Vec d | x ∈ U ∧ ¬euclideanBallAt x (2 * √↑d * 3 ^ (a + 1)) ⊆ U}

Every identity-grid row below the starting scale lies in a Euclidean inner boundary layer whose thickness is twice the Euclidean diameter bound for its escaping parent.

theorem HCPolySupport.HighContrast.volume_iUnion_fillingIndex_one_le {d : ℕ} (hd : 1 ≤ d) {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {rho Rad : ℝ} (hsand : HasBallSandwich U rho Rad) {n a : ℤ} (han : a < n) : MeasureTheory.volume (⋃ w ∈ Transport.fillingIndex 1 n U a, openCubeSet (translateCube w (originCube d a))) ≤ ENNReal.ofReal (6 * ↑d * √↑d * 3 ^ a / rho) * MeasureTheory.volume U

A convex Whitney row has the explicit boundary-volume rate 6 d^(3/2) 3^a / rho.

theorem HCPolySupport.HighContrast.volume_diff_iUnion_fillingIndex_one {d : ℕ} {U : Set (Vec d)} (hU : IsOpen U) (n : ℤ) : MeasureTheory.volume (U \ ⋃ a ∈ Set.Iic n, ⋃ w ∈ Transport.fillingIndex 1 n U a, openCubeSet (translateCube w (originCube d a))) = 0

The identity-grid maximal filling exhausts every open target up to a null set. Openness supplies a sufficiently fine cube around each point away from the countable union of grid faces.

theorem HCPolySupport.HighContrast.exists_convex_whitney_rows {d : ℕ} (hd : 1 ≤ d) {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {rho Rad : ℝ} (hsand : HasBallSandwich U rho Rad) (n : ℤ) : ∃ (Z : ℤ → Finset (Fin d → ℤ)), (∀ (a : ℤ), ↑(Z a) = Transport.fillingIndex 1 n U a) ∧ (∀ (a : ℤ), ∀ w ∈ Z a, openCubeSet (translateCube w (originCube d a)) ⊆ U) ∧ (∀ a < n, ∀ w ∈ Z a, ¬openCubeSet (translateCube (Transport.gridParent w) (originCube d (a + 1))) ⊆ U) ∧ (∀ (a b : ℤ), ∀ w ∈ Z a, ∀ v ∈ Z b, (a, w) ≠ (b, v) → Disjoint (openCubeSet (translateCube w (originCube d a))) (openCubeSet (translateCube v (originCube d b)))) ∧ (∀ a < n, ∑ w ∈ Z a, MeasureTheory.volume (openCubeSet (translateCube w (originCube d a))) ≤ ENNReal.ofReal (6 * ↑d * √↑d * 3 ^ a / rho) * MeasureTheory.volume U) ∧ MeasureTheory.volume (U \ ⋃ a ∈ Set.Iic n, ⋃ w ∈ ↑(Z a), openCubeSet (translateCube w (originCube d a))) = 0

A bounded open convex domain admits finite identity-grid Whitney rows with the exact open-triadic carriers, disjointness, parent escape, quantitative row volume, and almost-everywhere exhaustion.