High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Duality.AdaptedCellGaugeGeometry

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

The gauge image of an adapted-cell witness

The frozen Dirichlet domain premise exhibits U as an affine image of an open triadic cube,

U = (fun x => z + matVecMul L x) '' S,

with L the exact matrix root of the comparison matrix. Applying the gauge matImage L⁻¹ returns the cube itself, translated by matVecMul L⁻¹ z — the translation is by an arbitrary real vector, not by a lattice vector, so the gauge image is a translate of a triadic cube and not itself one.

theorem HCPolySupport.HighContrast.RowSupply.matImage_inv_affineImage {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) (z : Vec d) (S : Set (Vec d)) : matImage L⁻¹ ((fun (x : Vec d) => z + matVecMul L x) '' S) = translateSet (matVecMul L⁻¹ z) S

The gauge image of an adapted-cell witness is a translated cube.

theorem HCPolySupport.HighContrast.RowSupply.isOpen_translateSet {d : ℕ} {S : Set (Vec d)} (hS : IsOpen S) (z : Vec d) : IsOpen (translateSet z S)

Translates of open sets are open.

theorem HCPolySupport.HighContrast.RowSupply.isOpen_affineImage {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) (z : Vec d) {S : Set (Vec d)} (hS : IsOpen S) : IsOpen ((fun (x : Vec d) => z + matVecMul L x) '' S)

The affine image of an open set under an invertible matrix is open.