High-contrast homogenization: Provider.Regularity.RoundedAffineMap #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The rounded affine map for physical regularity transfer #
The rounded affine construction uses the base rounded grid. This module packages its positivity,
symmetry, invertibility, size, and lattice-alignment properties at the single
canonical generation kZero d.
theorem
HCPolySupport.HighContrast.isRoundedGrid_baseRoundedGrid
{d : ℕ}
{m : Mat d}
(hm : Matrix.PosDef m)
:
IsRoundedGrid (↑(kZero d)) (baseRoundedGrid m)
The base rounded grid is a rounded grid at its canonical alignment.
theorem
HCPolySupport.HighContrast.posDef_baseRoundedGrid
{d : ℕ}
{m : Mat d}
(hm : Matrix.PosDef m)
:
The rounded affine map remains positive definite.
theorem
HCPolySupport.HighContrast.matTranspose_baseRoundedGrid
{d : ℕ}
{m : Mat d}
(hm : Matrix.PosDef m)
:
The rounded affine map is symmetric.
theorem
HCPolySupport.HighContrast.isUnit_det_baseRoundedGrid
{d : ℕ}
{m : Mat d}
(hm : Matrix.PosDef m)
:
IsUnit (Matrix.det (baseRoundedGrid m))
The determinant of the rounded affine map is a unit.
theorem
HCPolySupport.HighContrast.norm_inv_baseRoundedGrid_le
{d : ℕ}
[NeZero d]
{m : Mat d}
(hm : Matrix.PosDef m)
:
The rounded affine inverse has a dimension-independent operator bound.