Documentation

LeanPool.HighContrastHomogenization.Provider.PolynomialHomogenization.Root.RowSupply.CommonResidualObservationParent

High-contrast homogenization: #

Provider.PolynomialHomogenization.Root.RowSupply.CommonResidualObservationParent

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

A common parent for residual-frame observation cells #

After the exact triadic part of the microscopic dilation has been removed, the residual affine grid is fixed and its scale lies in a compact interval. All ruled observation cubes are contained in the bounded gauge domain, so their affine images fit in one normalized-reference parent.

source
theorem HCPolySupport.HighContrast.RowSupply.residualObservationTarget_subset_matImage {d : ℕ} {U : Set (Vec d)} {rho Rad lambda : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (abar : Mat d) (i : system.CellIndex) :
adaptedCellTranslate (epsilonAffineGrid lambda abar) (ruledObservationCube system i).scale (lambda⁻¹ • matVecMul (matSqrt (symmPart abar)) (ruledObservationCenter system i) + adaptedCellCenter (epsilonAffineGrid lambda abar) (ruledObservationCube system i).scale 0) ⊆ matImage (epsilonAffineGrid lambda abar) U

A ruled observation target in residual affine coordinates is contained in the affine image of the gauge domain.