High-contrast homogenization: Provider.PolynomialHomogenization.Root.Corrector.AffineSandwichDepth

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

The affine sandwich depth for the centered cube exhaustion

The image of a centered exhaustion cube under a fixed matrix is contained in a centered exhaustion cube of a fixed larger index: the depth depends on the matrix alone, not on the cube. This is the geometric half of the carrier-level affine pullback.

def HCPolySupport.HighContrast.Root.matAbsTotal {d : ℕ} (L : Mat d) : ℝ

The total absolute mass of the entries of a matrix.

Equations

• HCPolySupport.HighContrast.Root.matAbsTotal L = ∑ i : Fin d, ∑ j : Fin d, |L i j|

theorem HCPolySupport.HighContrast.Root.row_abs_le_matAbsTotal {d : ℕ} (L : Mat d) (i : Fin d) : ∑ j : Fin d, |L i j| ≤ matAbsTotal L

theorem HCPolySupport.HighContrast.Root.abs_matVecMul_le_matAbsTotal_mul {d : ℕ} (L : Mat d) (x : Vec d) (i : Fin d) {c : ℝ} (hc : 0 ≤ c) (hx : ∀ (j : Fin d), |x j| ≤ c) : |matVecMul L x i| ≤ matAbsTotal L * c

Coordinates of a matrix image are bounded by the total absolute mass times the coordinate bound of the argument.

theorem HCPolySupport.HighContrast.Root.exists_matImage_localGradientCube_subset {d : ℕ} (L : Mat d) : ∃ (k : ℕ), ∀ (q : ℕ), matImage L (localGradientCube d q) ⊆ localGradientCube d (q + k)

The affine sandwich depth. For every matrix there is a fixed depth k such that the image of every centered exhaustion cube sits inside the centered exhaustion cube k steps coarser.