High-contrast homogenization: Provider.Response.CenteredResponseSchur

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

Schur-coordinate annealed identities

When the annealed coarse block is written in its positive Schur form, the annealed primal and adjoint energies and optimizer means have the explicit coordinate formulas used by the centered-response calculation.

theorem HCPolySupport.HighContrast.Response.matVecMul_eq_matrix_mulVec {d : ℕ} (A : Mat d) (x : Vec d) : matVecMul A x = Matrix.mulVec A x

The project and matrix-library notations for matrix-vector multiplication agree.

theorem HCPolySupport.HighContrast.Response.annealedBlock_eq_schur {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} (U : Book.Ch02.Domain d) {S SStar K : Mat d} (hE : toFullBlockMat (annealedBlock P U.carrier) = schurBlock S SStar K) : annealedBlock P U.carrier = ofFullBlockMat (schurBlock S SStar K)

Equality of flattened annealed blocks can be read as equality with the structural block induced by the Schur matrix.

theorem HCPolySupport.HighContrast.Response.ofFullBlockMat_schurBlock {d : ℕ} (S SStar K : Mat d) : ofFullBlockMat (schurBlock S SStar K) = { upperLeft := S + Matrix.conjTranspose K * SStar⁻¹ * K, upperRight := -(Matrix.conjTranspose K * SStar⁻¹), lowerLeft := -(SStar⁻¹ * K), lowerRight := SStar⁻¹ }

The structural form of a Schur block.

theorem HCPolySupport.HighContrast.Response.annealed_responseJ_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} (hE : toFullBlockMat (annealedBlock P U.carrier) = schurBlock S SStar K) (p q : Vec d) : ∫ (a : CoeffSpace d), Book.Ch02.responseJ U (a.coeffOn U) p q ∂P = 1 / 2 * p ⬝ᵥ Matrix.mulVec S p + 1 / 2 * (q + Matrix.mulVec K p) ⬝ᵥ SStar⁻¹.mulVec (q + Matrix.mulVec K p) - vecDot p q

The primal annealed response energy in Schur coordinates.

theorem HCPolySupport.HighContrast.Response.annealed_adjoint_responseJ_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} (hE : toFullBlockMat (annealedBlock P U.carrier) = schurBlock S SStar K) (p q : Vec d) : ∫ (a : CoeffSpace d), Book.Ch02.responseJ U (a.transpose.coeffOn U) p q ∂P = 1 / 2 * p ⬝ᵥ Matrix.mulVec S p + 1 / 2 * (q - Matrix.mulVec K p) ⬝ᵥ SStar⁻¹.mulVec (q - Matrix.mulVec K p) - vecDot p q

The adjoint annealed response energy in the original Schur coordinates.

theorem HCPolySupport.HighContrast.Response.blockR_schur_mulVec_primal {d : ℕ} (S SStar K : Mat d) (p q : Vec d) : blockMatVecMul (Book.Ch02.blockR d) (blockMatVecMul (ofFullBlockMat (schurBlock S SStar K)) (-p, q)) + (-p, q) = (-p + SStar⁻¹.mulVec (q + Matrix.mulVec K p), (1 - Matrix.conjTranspose K * SStar⁻¹).mulVec q - Matrix.mulVec (S + Matrix.conjTranspose K * SStar⁻¹ * K) p)

The two rows of the Schur block applied to the primal signed load.

theorem HCPolySupport.HighContrast.Response.blockR_adjoint_schur_mulVec {d : ℕ} (S SStar K : Mat d) (p q : Vec d) : blockMatVecMul (Book.Ch02.blockR d) (blockMatVecMul (Book.Ch02.blockMatMul (Book.Ch02.blockDiag 1 (-1)) (Book.Ch02.blockMatMul (ofFullBlockMat (schurBlock S SStar K)) (Book.Ch02.blockDiag 1 (-1)))) (-p, q)) + (-p, q) = (-p + SStar⁻¹.mulVec (q - Matrix.mulVec K p), (1 + Matrix.conjTranspose K * SStar⁻¹).mulVec q - Matrix.mulVec (S + Matrix.conjTranspose K * SStar⁻¹ * K) p)

The two rows of the signed Schur block applied to the adjoint load.

theorem HCPolySupport.HighContrast.Response.annealed_optimizer_means_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} (hE : toFullBlockMat (annealedBlock P U.carrier) = schurBlock S SStar K) (p q : Vec d) : (annealedOptimizerGradient P U p q, annealedOptimizerFlux P U p q) = (-p + SStar⁻¹.mulVec (q + Matrix.mulVec K p), (1 - Matrix.conjTranspose K * SStar⁻¹).mulVec q - Matrix.mulVec (S + Matrix.conjTranspose K * SStar⁻¹ * K) p)

The two separately annealed primal optimizer means in Schur coordinates.

theorem HCPolySupport.HighContrast.Response.annealed_adjoint_optimizer_means_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} (hE : toFullBlockMat (annealedBlock P U.carrier) = schurBlock S SStar K) (p q : Vec d) : (annealedAdjointOptimizerGradient P U p q, annealedAdjointOptimizerFlux P U p q) = (-p + SStar⁻¹.mulVec (q - Matrix.mulVec K p), (1 + Matrix.conjTranspose K * SStar⁻¹).mulVec q - Matrix.mulVec (S + Matrix.conjTranspose K * SStar⁻¹ * K) p)

The two separately annealed adjoint optimizer means in Schur coordinates.