High-contrast homogenization: Provider.PolynomialHomogenization.NormalizedResponseExcess #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Normalized response bounded by block excess #
The intrinsic normalization of the doubled response uses a load P with unit
quadratic energy in the constant comparison block and pairs it with the dual
load obtained by applying that block. The doubled splitting then bounds both
quadratic terms by the same one-sided excess. This formulation avoids choosing
coordinates for the positive square root and is stable under the affine and
constant-skew changes of variables used later.
theorem
HCPolySupport.HighContrast.doubledResponseJ_le_blockExcess_of_constantBlockQuadratic_eq_one
{d : ℕ}
{U : Book.Ch02.Domain d}
(a : Book.Ch02.CoeffOn U)
{a0 : Mat d}
(ha0 : Matrix.PosDef (symmPart a0))
(P : BlockVec d)
(hquad : blockVecDot P (blockMatVecMul (Book.Ch02.constantBlockMatrix a0) P) = 1)
:
A doubled response at an intrinsically normalized load is bounded by the one-sided excess of its coarse block over the constant comparison block.