High-contrast homogenization: Provider.Regularity.EnlargedMarginDatumRegularity

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

Observation-datum regularity from enlarged Whitney margins

The ninefold admissibility buffer places both the closure of the observation cube and that cube itself inside the strict inner half of the next centered triadic cube. This supplies the geometric hypotheses of the constant- coefficient datum regularity theorem after translating a selected cell to the origin.

noncomputable def HCPolySupport.HighContrast.enlargedMarginObservationCenter {d : ℕ} {U : Set (Vec d)} {rho Rad : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (i : system.CellIndex) : Vec d

The center used to view an enlarged-margin cell from the origin.

Equations

• HCPolySupport.HighContrast.enlargedMarginObservationCenter system i = HCPolySupport.HighContrast.standardCellCenter (system.scale i) (system.index i)

def HCPolySupport.HighContrast.enlargedMarginAmbientCube {d : ℕ} {U : Set (Vec d)} {rho Rad : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (i : system.CellIndex) : TriadicCube d

The ambient cube furnished by ninefold admissibility is one scale larger than the observation cube.

Equations

• HCPolySupport.HighContrast.enlargedMarginAmbientCube system i = HCPolySupport.originCube d (system.scale i + 2)

theorem HCPolySupport.HighContrast.interiorBuffer_eq_translateSet_ambientCube {d : ℕ} {U : Set (Vec d)} {rho Rad : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (i : system.CellIndex) : system.interiorBuffer i = translateSet (enlargedMarginObservationCenter system i) (openCubeSet (enlargedMarginAmbientCube system i))

The enlarged admissibility buffer is the translated ambient cube.