High-contrast homogenization: Provider.Response.ConstantSkewHistory #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Constant-skew invariance of nonlinear histories and drift #
Common shear congruence preserves the trace of a relative mean, determinant increments, and the inverse-times-increment trace used by the fixed-grid drift. These identities complete the passage between hatted terminal data and the portable histories.
theorem
HCPolySupport.HighContrast.Response.trace_inv_mul_skewBlockCongr
{d : ℕ}
(g : Mat d)
(A E : BlockMat d)
:
((toFullBlockMat (skewBlockCongr g E))⁻¹ * toFullBlockMat (skewBlockCongr g A)).trace = ((toFullBlockMat E)⁻¹ * toFullBlockMat A).trace
The trace of inverse times numerator is invariant under a common shear congruence.