High-contrast homogenization: Provider.Quenched.SmallContrastCenteringAdjointIdentity

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

The closed form of the adjoint centering pairing

The adjoint mirror of the centering-pairing identity: at the recentered samples of the transposed coefficient, the pairing of the two annealed adjoint optimizer averages has a closed form in the Schur data of the annealed block. It is the primal closed form with the symmetric skew coordinate negated.

theorem HCPolySupport.HighContrast.Quenched.centering_adjoint_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) ⋯).transpose.coeffOn U) (Response.centeredAdjointOptimizer 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) ⋯).transpose.coeffOn U) (Response.centeredAdjointOptimizer 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 adjoint centering pairing in closed Schur form.