High-contrast homogenization: Provider.Response.ConstantSkewCentered

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

Constant-skew covariance of centered responses

The canonical optimizer for the recentered coefficient has the same gradient as the canonical optimizer for the original coefficient with the corrected second load. Its averaged flux is shifted by the constant skew matrix applied to its averaged gradient. This records the covariance of the two separate annealed centering factors.

theorem HCPolySupport.HighContrast.Response.centeredResponseOptimizer_subSkew_gradient_ae {d : ℕ} (U : Book.Ch02.Domain d) (a : CoeffSpace d) (g : Mat d) (hg : IsSkewMat g) (p q : Vec d) : (centeredResponseOptimizer U (a.subSkew g hg) p q).toH1.grad =ᵐ[volumeMeasureOn U.carrier] (centeredResponseOptimizer U a p (q - matVecMul g p)).toH1.grad

The canonical shifted optimizer and the original optimizer at the corrected load have the same gradient almost everywhere.

theorem HCPolySupport.HighContrast.Response.averageGradient_centeredResponseOptimizer_subSkew {d : ℕ} (U : Book.Ch02.Domain d) (a : CoeffSpace d) (g : Mat d) (hg : IsSkewMat g) (p q : Vec d) : Book.Ch02.averageGradient U ((a.subSkew g hg).coeffOn U) (centeredResponseOptimizer U (a.subSkew g hg) p q) = Book.Ch02.averageGradient U (a.coeffOn U) (centeredResponseOptimizer U a p (q - matVecMul g p))

The spatially averaged gradient is unchanged by constant-skew recentering, after correcting the second load.

theorem HCPolySupport.HighContrast.Response.averageFlux_centeredResponseOptimizer_subSkew {d : ℕ} (U : Book.Ch02.Domain d) (a : CoeffSpace d) (g : Mat d) (hg : IsSkewMat g) (p q : Vec d) : Book.Ch02.averageFlux U ((a.subSkew g hg).coeffOn U) (centeredResponseOptimizer U (a.subSkew g hg) p q) = Book.Ch02.averageFlux U (a.coeffOn U) (centeredResponseOptimizer U a p (q - matVecMul g p)) - matVecMul g (Book.Ch02.averageGradient U (a.coeffOn U) (centeredResponseOptimizer U a p (q - matVecMul g p)))

The averaged optimizer flux changes by -g times the averaged gradient.