High-contrast homogenization: Provider.Response.CenteredResponseFormulas

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

Centered response formulas

The centered primal and adjoint responses have explicit formulas in the Schur coordinates of the annealed coarse block. Adding them at the two shifted loads gives the nonsymmetric polarization identity used by the response estimate.

theorem HCPolySupport.HighContrast.Response.centeredResponse_eq_schur {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 q : Vec d) : centeredResponse P U p q = 1 / 2 * (q + Matrix.mulVec K p) ⬝ᵥ (SStar⁻¹ * K * SStar⁻¹).mulVec (q + Matrix.mulVec K p) + 1 / 2 * (SStar⁻¹ * S).mulVec p ⬝ᵥ (q + Matrix.mulVec K p) - 1 / 2 * p ⬝ᵥ q

The corrected centered primal response formula.

theorem HCPolySupport.HighContrast.Response.centeredAdjointResponse_eq_schur {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 q : Vec d) : centeredAdjointResponse P U p q = -(1 / 2) * (q - Matrix.mulVec K p) ⬝ᵥ (SStar⁻¹ * K * SStar⁻¹).mulVec (q - Matrix.mulVec K p) + 1 / 2 * (SStar⁻¹ * S).mulVec p ⬝ᵥ (q - Matrix.mulVec K p) - 1 / 2 * p ⬝ᵥ q

The corrected centered adjoint response formula. Its leading term has the opposite sign because coefficient transposition sends K to -K.

theorem HCPolySupport.HighContrast.Response.centeredResponse_add_adjoint_eq_schur {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (U : Book.Ch02.Domain d) (hint : HasIntegrableCoarseBlock P U.carrier) {S SStar K : Mat d} (hS : Matrix.PosDef S) (hStar : Matrix.PosDef SStar) (hE : toFullBlockMat (annealedBlock P U.carrier) = schurBlock S SStar K) (p q r : Vec d) : centeredResponse P U p (q - r) + centeredAdjointResponse P U p (q + r) = p ⬝ᵥ (S * SStar⁻¹ - 1).mulVec q + (Matrix.mulVec K p - r) ⬝ᵥ (SStar⁻¹ * (K + Matrix.conjTranspose K) * SStar⁻¹).mulVec q

Adding the primal and adjoint formulas at opposite load shifts gives the corrected nonsymmetric polarization identity.