High-contrast homogenization: #
Provider.PolynomialHomogenization.Root.RowSupply.RealTranslationDoubledResponse
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Real-translation covariance of the doubled response #
The deterministic coarse response is covariant under every Euclidean translation. No invariance of a probability law is asserted here.
theorem
HCPolySupport.HighContrast.RowSupply.coarseBlock_translateSet_real
{d : ℕ}
(z : Vec d)
(U : Set (Vec d))
(a : CoeffSpace d)
:
Coarse blocks on a translated set are coarse blocks of the deterministically translated coefficient sample.
theorem
HCPolySupport.HighContrast.RowSupply.coeffSpaceDoubledResponse_translateSet_real
{d : ℕ}
(z : Vec d)
(U : Set (Vec d))
(a : CoeffSpace d)
(P Q : BlockVec d)
:
Transport.coeffSpaceDoubledResponse (translateSet z U) a P Q = Transport.coeffSpaceDoubledResponse U (realTranslateCoeff z a) P Q
The coefficient-space doubled response is covariant under arbitrary real translations.