High-contrast homogenization: Provider.Quenched.SmallContrastCenteringEstimate #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The generic centering estimate #
The closed Schur form of the centering pairing, at the calibrated loads of
the response metric, is second order in the contrast defect: the calibration
defect is the B⁻¹-quadratic of (B−1)e, the symmetric-skew terms cancel to
their quadratic remainder, and the diagonal-gap term pairs against the
deviation vector. The hypotheses are the normalized diagonal gap, the
symmetric-skew bound, and their two trace forms; the conclusion holds with
the dimension-only constant 6d + 8.
theorem
HCPolySupport.HighContrast.Quenched.centering_generic_estimate
{d : ℕ}
{S SStar κ : Mat d}
(hS : Matrix.PosDef S)
(hStar : Matrix.PosDef SStar)
(hκ : Matrix.conjTranspose κ = κ)
{eps : ℝ}
(heps0 : 0 ≤ eps)
(heps1 : eps ≤ 1)
(horder : SStar ≤ S)
(hgapM : S - SStar ≤ eps • SStar)
(hskewM : κ * SStar⁻¹ * κ ≤ (eps ^ 2 / 4) • SStar)
(htrGap : ((S - SStar) * SStar⁻¹).trace ≤ eps)
(htrSkew : (κ * SStar⁻¹ * κ * SStar⁻¹).trace ≤ ↑d * eps ^ 2 / 4)
(e : Vec d)
(he : e ⬝ᵥ e = 1)
:
|(matSqrt (matGeomMean (S + κ * SStar⁻¹ * κ) SStar)⁻¹).mulVec e ⬝ᵥ Matrix.mulVec S ((matSqrt (matGeomMean (S + κ * SStar⁻¹ * κ) SStar)⁻¹).mulVec e) + ((matSqrt (matGeomMean (S + κ * SStar⁻¹ * κ) SStar)).mulVec e + Matrix.mulVec κ ((matSqrt (matGeomMean (S + κ * SStar⁻¹ * κ) SStar)⁻¹).mulVec e)) ⬝ᵥ SStar⁻¹.mulVec
((matSqrt (matGeomMean (S + κ * SStar⁻¹ * κ) SStar)).mulVec e + Matrix.mulVec κ ((matSqrt (matGeomMean (S + κ * SStar⁻¹ * κ) SStar)⁻¹).mulVec e)) - (matSqrt (matGeomMean (S + κ * SStar⁻¹ * κ) SStar)⁻¹).mulVec e ⬝ᵥ (matSqrt (matGeomMean (S + κ * SStar⁻¹ * κ) SStar)).mulVec e - SStar⁻¹.mulVec
((matSqrt (matGeomMean (S + κ * SStar⁻¹ * κ) SStar)).mulVec e + Matrix.mulVec κ ((matSqrt (matGeomMean (S + κ * SStar⁻¹ * κ) SStar)⁻¹).mulVec e)) ⬝ᵥ Matrix.mulVec κ
(SStar⁻¹.mulVec
((matSqrt (matGeomMean (S + κ * SStar⁻¹ * κ) SStar)).mulVec e + Matrix.mulVec κ ((matSqrt (matGeomMean (S + κ * SStar⁻¹ * κ) SStar)⁻¹).mulVec e))) - Matrix.mulVec S ((matSqrt (matGeomMean (S + κ * SStar⁻¹ * κ) SStar)⁻¹).mulVec e) ⬝ᵥ SStar⁻¹.mulVec
((matSqrt (matGeomMean (S + κ * SStar⁻¹ * κ) SStar)).mulVec e + Matrix.mulVec κ ((matSqrt (matGeomMean (S + κ * SStar⁻¹ * κ) SStar)⁻¹).mulVec e))| ≤ (6 * ↑d + 8) * eps ^ 2
The generic centering estimate. κ is the symmetric skew coordinate;
the primal pairing consumes it as stated and the adjoint pairing at −κ.