High-contrast homogenization: Provider.PolynomialHomogenization.RuledPairingSplit

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

theorem HCPolySupport.HighContrast.iUnion_whitneyCells_eq_rows {d : ℕ} {U : Set (Vec d)} {rho Rad : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) : ⋃ (i : system.CellIndex), system.cell i = ⋃ (a : ℤ), ⋃ w ∈ ↑(system.rows a), standardCell d a w

The union over the ruled cell index is the union over all scale rows.

theorem HCPolySupport.HighContrast.iUnion_whitneyCells_ae_eq_domain {d : ℕ} {U : Set (Vec d)} {rho Rad : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (hd : 1 ≤ d) (hU : IsOpenBoundedConvexDomain U) : ⋃ (i : system.CellIndex), system.cell i =ᵐ[MeasureTheory.volume] U

The ruled Whitney cells exhaust the domain up to a null set.

theorem HCPolySupport.HighContrast.pairwise_disjoint_whitneyCells {d : ℕ} {U : Set (Vec d)} {rho Rad : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) : Pairwise (Function.onFun Disjoint fun (i : system.CellIndex) => system.cell i)

Distinct ruled indices represent disjoint cell interiors.

theorem HCPolySupport.HighContrast.measurableSet_whitneyCell {d : ℕ} {U : Set (Vec d)} {rho Rad : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (i : system.CellIndex) : MeasurableSet (system.cell i)

Every ruled Whitney cell is measurable.