High-contrast homogenization: Provider.PolynomialHomogenization.ConvexHardyWhitneySystem

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

Whitney rows with coherent convex Hardy chains

A ball-sandwiched convex domain admits maximal triadic Whitney rows together with one coherent interior-ball chain for every selected cell. The top row is chosen at the inner-ball scale, all chains use the same sandwich center, and distinct rows have distinct dyadic chain lengths.

structure HCPolySupport.HighContrast.ConvexHardyWhitneySystem {d : ℕ} (U : Set (Vec d)) (rho Rad : ℝ) : Type

Maximal Whitney rows equipped with coherent chains to one fixed inner ball.

• center : Vec d

  Common center of the inner and outer balls bounding U.

• inner_ball : euclideanBallAt self.center rho ⊆ U
• outer_ball : U ⊆ euclideanBallAt self.center Rad
• topScale : ℤ

  Whitney cutoff generation satisfying 3 ^ topScale ≤ rho < 3 ^ (topScale + 1).

• topScale_lower : 3 ^ self.topScale ≤ rho
• topScale_upper : rho < 3 ^ (self.topScale + 1)
• rows : ℤ → Finset (Fin d → ℤ)

  Finite grid indices of the maximal Euclidean Whitney cells in each generation.

• rows_eq (a : ℤ) : ↑(self.rows a) = Transport.fillingIndex 1 self.topScale U a
• cell_subset (a : ℤ) (w : Fin d → ℤ) : w ∈ self.rows a → standardCell d a w ⊆ U
• parent_escape (a : ℤ) : a < self.topScale → ∀ w ∈ self.rows a, ¬standardCell d (a + 1) (Transport.gridParent w) ⊆ U
• pairwise_disjoint (a b : ℤ) (w : Fin d → ℤ) : w ∈ self.rows a → ∀ v ∈ self.rows b, (a, w) ≠ (b, v) → Disjoint (standardCell d a w) (standardCell d b v)
• row_volume (a : ℤ) : a < self.topScale → ∑ w ∈ self.rows a, MeasureTheory.volume (standardCell d a w) ≤ ENNReal.ofReal (6 * ↑d * √↑d * 3 ^ a / rho) * MeasureTheory.volume U
• ae_exhaustion : MeasureTheory.volume (U \ ⋃ a ∈ Set.Iic self.topScale, ⋃ w ∈ ↑(self.rows a), standardCell d a w) = 0
• chainLength : { a : ℤ // a ≤ self.topScale } → ℕ

  Length shared by the Hardy ball chains in each Whitney generation.

• chainLength_bounds (a : { a : ℤ // a ≤ self.topScale }) : 3 ^ ↑a ≤ convexHardyBallChainRadius rho (self.chainLength a) 0 ∧ convexHardyBallChainRadius rho (self.chainLength a) 0 < 2 * 3 ^ ↑a
• chainLength_injective : Function.Injective self.chainLength
• chain (a : { a : ℤ // a ≤ self.topScale }) (w : ↥(self.rows ↑a)) : ConvexHardyBallChain U (standardCellCenter ↑a ↑w) rho Rad (3 ^ ↑a)

  A Hardy ball chain from each selected cell center to the common inner ball.

• chain_center (a : { a : ℤ // a ≤ self.topScale }) (w : ↥(self.rows ↑a)) : (self.chain a w).center = self.center
• chain_length (a : { a : ℤ // a ≤ self.topScale }) (w : ↥(self.rows ↑a)) : (self.chain a w).length = self.chainLength a

theorem HCPolySupport.HighContrast.exists_convexHardyWhitneySystem {d : ℕ} (hd : 1 ≤ d) {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {rho Rad : ℝ} (hsand : HasBallSandwich U rho Rad) : Nonempty (ConvexHardyWhitneySystem U rho Rad)

Every ball-sandwiched bounded open convex domain has coherent maximal Whitney rows and straight chains to a common inner ball.