High-contrast homogenization: Provider.Quenched.SmallContrastCenteringIdentity

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

The closed form of the centering pairing

The centering term of the compact response reabsorption is the pairing of the two annealed optimizer averages at the recentered samples. Constant-skew covariance and the two annealed Schur formulas give it a closed form in the Schur data of the annealed block: every appearance of the antisymmetric skew part cancels, leaving an expression in the symmetric skew coordinate alone.

theorem HCPolySupport.HighContrast.Quenched.centering_pairing_eq {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (U : Book.Ch02.Domain d) (hint : HasIntegrableCoarseBlock P U.carrier) {S SStar K : Mat d} (hStar : Matrix.PosDef SStar) (hE : toFullBlockMat (annealedBlock P U.carrier) = schurBlock S SStar K) (p r : Vec d) : (vecDot (fun (i : Fin d) => ∫ (a : CoeffSpace d), Book.Ch02.averageGradient U ((a.subSkew (Response.responseSkew K) ⋯).coeffOn U) (Response.centeredResponseOptimizer U (a.subSkew (Response.responseSkew K) ⋯) p r) i ∂P) fun (i : Fin d) => ∫ (a : CoeffSpace d), Book.Ch02.averageFlux U ((a.subSkew (Response.responseSkew K) ⋯).coeffOn U) (Response.centeredResponseOptimizer U (a.subSkew (Response.responseSkew K) ⋯) p r) i ∂P) = p ⬝ᵥ Matrix.mulVec S p + (r + Matrix.mulVec (Response.responseSymmetric K) p) ⬝ᵥ SStar⁻¹.mulVec (r + Matrix.mulVec (Response.responseSymmetric K) p) - p ⬝ᵥ r - (r + Matrix.mulVec (Response.responseSymmetric K) p) ⬝ᵥ (SStar⁻¹ * K * SStar⁻¹).mulVec (r + Matrix.mulVec (Response.responseSymmetric K) p) - (SStar⁻¹ * S).mulVec p ⬝ᵥ (r + Matrix.mulVec (Response.responseSymmetric K) p)

The centering pairing in closed Schur form.