High-contrast homogenization: Provider.PolynomialHomogenization.RuledObservationComparisonPricing

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

Observation-cube comparison pricing on ruled Whitney cells

Each ruled cell is viewed from the center of its concentric threefold interior buffer. The comparison problem is solved on the resulting origin-centered observation cube. Its priced fields are then evaluated on the translated copy of the ruled cell, which is covered by the canonical depth-one child cores.

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

The physical center used to translate one ruled cell to the origin.

Equations

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

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

The origin-centered observation cube is one generation larger than the ruled cell.

Equations

• HCPolySupport.HighContrast.ruledObservationCube system i = HCPolySupport.originCube d (system.scale i + 1)

theorem HCPolySupport.HighContrast.translateSet_observationCube_subset_interiorBuffer {d : ℕ} {U : Set (Vec d)} {rho Rad : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (i : system.CellIndex) : translateSet (ruledObservationCenter system i) (openCubeSet (ruledObservationCube system i)) ⊆ system.interiorBuffer i

The translated observation cube lies in the enlarged ruled interior buffer.