High-contrast homogenization: Provider.Response.ConstantSkewBlock

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

Constant-skew congruence of coarse blocks

Subtracting a constant skew matrix from a coefficient sample conjugates its coarse response by the corresponding lower triangular shear. This file proves that covariance from the response functional and then records its adapted-cell and annealed consequences.

def HCPolySupport.HighContrast.Response.skewBlockCongr {d : ℕ} (g : Mat d) (A : BlockMat d) : BlockMat d

Congruence of a doubled block by the constant-skew shear.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.Response.toFullBlockMat_skewBlockCongr {d : ℕ} (g : Mat d) (A : BlockMat d) : toFullBlockMat (skewBlockCongr g A) = Matrix.conjTranspose (fullBlockShear g) * toFullBlockMat A * fullBlockShear g

Flattening exposes constant-skew congruence as ordinary matrix congruence.

theorem HCPolySupport.HighContrast.Response.blockVector_skewShift {d : ℕ} (g : Mat d) (X : BlockVec d) : Matrix.mulVec (fullBlockShear g) (toFullBlockVec X) = toFullBlockVec (X.1, matVecMul g X.1 + X.2)

The shear sends (x,y) to (x,gx+y).

theorem HCPolySupport.HighContrast.Response.blockQuadratic_skewBlockCongr {d : ℕ} (g : Mat d) (A : BlockMat d) (X : BlockVec d) : blockVecDot X (blockMatVecMul (skewBlockCongr g A) X) = blockVecDot (X.1, matVecMul g X.1 + X.2) (blockMatVecMul A (X.1, matVecMul g X.1 + X.2))

A skew congruence reads the original quadratic form at the shifted doubled vector.

theorem HCPolySupport.HighContrast.Response.isSymmetricBlockMat_skewBlockCongr {d : ℕ} {g : Mat d} {A : BlockMat d} (hA : IsSymmetricBlockMat A) : IsSymmetricBlockMat (skewBlockCongr g A)

Congruence preserves symmetry.

theorem HCPolySupport.HighContrast.Response.blockPosDef_skewBlockCongr {d : ℕ} {g : Mat d} {A : BlockMat d} (hA : Book.Ch02.BlockPosDef A) : Book.Ch02.BlockPosDef (skewBlockCongr g A)

Congruence by a shear preserves positive definiteness.

theorem HCPolySupport.HighContrast.Response.blockQuadratic_coarseBlock_subSkew {d : ℕ} (U : Book.Ch02.Domain d) (a : CoeffSpace d) (g : Mat d) (hg : IsSkewMat g) (X : BlockVec d) : blockVecDot X (blockMatVecMul (coarseBlock U.carrier (a.subSkew g hg)) X) = blockVecDot (X.1, matVecMul g X.1 + X.2) (blockMatVecMul (coarseBlock U.carrier a) (X.1, matVecMul g X.1 + X.2))

The quadratic form of the recentered coarse response is the original quadratic form at the shear-shifted doubled vector.

theorem HCPolySupport.HighContrast.Response.coarseBlock_subSkew {d : ℕ} (U : Book.Ch02.Domain d) (a : CoeffSpace d) (g : Mat d) (hg : IsSkewMat g) : coarseBlock U.carrier (a.subSkew g hg) = skewBlockCongr g (coarseBlock U.carrier a)

Constant-skew covariance of the coarse response.

theorem HCPolySupport.HighContrast.Response.adaptedResponse_subSkew {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (k : ℤ) (w : Fin d → ℤ) (a : CoeffSpace d) (g : Mat d) (hg : IsSkewMat g) : adaptedResponse q k w (a.subSkew g hg) = skewBlockCongr g (adaptedResponse q k w a)

Constant-skew covariance on a translated adapted cell.

theorem HCPolySupport.HighContrast.Response.integral_coarseBlock_subSkew {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} (U : Book.Ch02.Domain d) (hint : HasIntegrableCoarseBlock P U.carrier) (g : Mat d) (hg : IsSkewMat g) : ∫ (a : CoeffSpace d), toFullBlockMat (coarseBlock U.carrier (a.subSkew g hg)) ∂P = toFullBlockMat (skewBlockCongr g (annealedBlock P U.carrier))

The expected recentered coarse response is the congruence of the annealed block.