High-contrast homogenization: Provider.Quenched.SmallContrastCenterMagnitude

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

The center magnitudes

Both components of the annealed center at the calibrated loads — the closed Schur forms of the annealed mean gradient and mean flux — are second order in the smallness parameter: the mean gradient is the deviation vector δ of the centering estimate, and the mean flux is the calibration bracket deviation plus a skew-small correction. This is the printed |M₀^{1/2}𝔼[(∇v)_{□}]|² ≤ C(Θ̂−1)² display, feeding the row cap at the profile centers.

theorem HCPolySupport.HighContrast.Quenched.centering_center_quads_le {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 + SStar⁻¹.mulVec ((matSqrt (matGeomMean (S + κ * SStar⁻¹ * κ) SStar)).mulVec e + Matrix.mulVec κ ((matSqrt (matGeomMean (S + κ * SStar⁻¹ * κ) SStar)⁻¹).mulVec e))) ⬝ᵥ Matrix.mulVec SStar (-(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))) ≤ 5 * (1 + ↑d) * eps ^ 2 ∧ ((1 - κ * SStar⁻¹).mulVec ((matSqrt (matGeomMean (S + κ * SStar⁻¹ * κ) SStar)).mulVec e) - Matrix.mulVec (S + κ * SStar⁻¹ * κ) ((matSqrt (matGeomMean (S + κ * SStar⁻¹ * κ) SStar)⁻¹).mulVec e)) ⬝ᵥ SStar⁻¹.mulVec ((1 - κ * SStar⁻¹).mulVec ((matSqrt (matGeomMean (S + κ * SStar⁻¹ * κ) SStar)).mulVec e) - Matrix.mulVec (S + κ * SStar⁻¹ * κ) ((matSqrt (matGeomMean (S + κ * SStar⁻¹ * κ) SStar)⁻¹).mulVec e)) ≤ 24 * (1 + ↑d) * eps ^ 2

The center magnitudes. At the calibrated loads, both components of the annealed center — the closed Schur forms of the mean gradient and mean flux — are second order in ε, in the natural σ*-metrics.