High-contrast homogenization: Provider.Response.AffineResponseGeometry

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

Response averages on an adapted cell

The inverse grid map identifies an adapted cell with its centered reference cube. The determinant occurring in the integral change of variables also occurs in the cell volume, so normalized scalar and vector averages have no Jacobian factor.

theorem HCPolySupport.HighContrast.matImage_inv_adaptedCell_eq_centeredCube {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) : matImage q⁻¹ (adaptedCell q t) = centeredCube d t

The inverse grid map sends an adapted cell to its centered reference cube.

theorem HCPolySupport.HighContrast.adaptedCell_eq_matVecMul_image_openCubeSet {d : ℕ} (q : Mat d) (t : ℤ) : adaptedCell q t = matVecMul q '' openCubeSet (originCube d t)

An adapted cell is literally the grid image of its reference origin cube.

theorem HCPolySupport.HighContrast.adaptedPreYoungCutoff_pullback_hasCompactSupport {d : ℕ} {q : Mat d} [NeZero d] (hq : Matrix.PosDef q) (t : ℤ) : HasCompactSupport fun (y : Vec d) => Response.adaptedPreYoungCutoff q hq t (matVecMul q y)

Pulling the adapted cutoff back by its invertible grid preserves compact support.

theorem HCPolySupport.HighContrast.adaptedPreYoungCutoff_pullback_tsupport_subset_openCubeSet {d : ℕ} {q : Mat d} [NeZero d] (hq : Matrix.PosDef q) (t : ℤ) : (tsupport fun (y : Vec d) => Response.adaptedPreYoungCutoff q hq t (matVecMul q y)) ⊆ openCubeSet (originCube d t)

The support of the pulled-back adapted cutoff lies in the reference origin cube.

theorem HCPolySupport.HighContrast.average_adaptedDomain_eq_cubeAverage_pullback {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (f : Vec d → ℝ) : Book.Ch02.average (Response.adaptedDomain hq t) f = cubeAverage (originCube d t) fun (y : Vec d) => f (matVecMul q y)

A normalized scalar average on an adapted domain is the cube average of the pullback by the grid map.