High-contrast homogenization: Provider.Response.ConstantSkewAdjoint

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

Constant-skew covariance for the adjoint response

Transposition reverses the sign of a skew recentering. The adjoint optimizer therefore has the opposite load correction and flux shift from the primal optimizer, while its centered response is again unchanged.

theorem HCPolySupport.HighContrast.Response.averageGradient_centeredAdjointOptimizer_subSkew {d : ℕ} (U : Book.Ch02.Domain d) (a : CoeffSpace d) (g : Mat d) (hg : IsSkewMat g) (p q : Vec d) : Book.Ch02.averageGradient U ((a.subSkew g hg).transpose.coeffOn U) (centeredAdjointOptimizer U (a.subSkew g hg) p q) = Book.Ch02.averageGradient U (a.transpose.coeffOn U) (centeredAdjointOptimizer U a p (q + matVecMul g p))

The averaged adjoint optimizer gradient is unchanged after applying the oppositely signed load correction.

theorem HCPolySupport.HighContrast.Response.averageFlux_centeredAdjointOptimizer_subSkew {d : ℕ} (U : Book.Ch02.Domain d) (a : CoeffSpace d) (g : Mat d) (hg : IsSkewMat g) (p q : Vec d) : Book.Ch02.averageFlux U ((a.subSkew g hg).transpose.coeffOn U) (centeredAdjointOptimizer U (a.subSkew g hg) p q) = Book.Ch02.averageFlux U (a.transpose.coeffOn U) (centeredAdjointOptimizer U a p (q + matVecMul g p)) + matVecMul g (Book.Ch02.averageGradient U (a.transpose.coeffOn U) (centeredAdjointOptimizer U a p (q + matVecMul g p)))

The averaged adjoint optimizer flux gains the skew matrix applied to the averaged adjoint optimizer gradient.

theorem HCPolySupport.HighContrast.Response.annealedAdjointOptimizerGradient_subSkew {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} (U : Book.Ch02.Domain d) (g : Mat d) (hg : IsSkewMat g) (p q : Vec d) : (fun (i : Fin d) => ∫ (a : CoeffSpace d), Book.Ch02.averageGradient U ((a.subSkew g hg).transpose.coeffOn U) (centeredAdjointOptimizer U (a.subSkew g hg) p q) i ∂P) = annealedAdjointOptimizerGradient P U p (q + matVecMul g p)

The separately annealed adjoint optimizer gradient has the positive load correction associated with coefficient transposition.

theorem HCPolySupport.HighContrast.Response.annealedAdjointOptimizerFlux_subSkew {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (U : Book.Ch02.Domain d) (hint : HasIntegrableCoarseBlock P U.carrier) (g : Mat d) (hg : IsSkewMat g) (p q : Vec d) : (fun (i : Fin d) => ∫ (a : CoeffSpace d), Book.Ch02.averageFlux U ((a.subSkew g hg).transpose.coeffOn U) (centeredAdjointOptimizer U (a.subSkew g hg) p q) i ∂P) = annealedAdjointOptimizerFlux P U p (q + matVecMul g p) + matVecMul g (annealedAdjointOptimizerGradient P U p (q + matVecMul g p))

The separately annealed adjoint optimizer flux gains the skew matrix applied to the annealed adjoint optimizer gradient.

theorem HCPolySupport.HighContrast.Response.centeredAdjointResponse_subSkew {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (U : Book.Ch02.Domain d) (hint : HasIntegrableCoarseBlock P U.carrier) (g : Mat d) (hg : IsSkewMat g) (p q : Vec d) : (∫ (a : CoeffSpace d), Book.Ch02.responseJ U ((a.subSkew g hg).transpose.coeffOn U) p q ∂P - 1 / 2 * vecDot (fun (i : Fin d) => ∫ (a : CoeffSpace d), Book.Ch02.averageGradient U ((a.subSkew g hg).transpose.coeffOn U) (centeredAdjointOptimizer U (a.subSkew g hg) p q) i ∂P) fun (i : Fin d) => ∫ (a : CoeffSpace d), Book.Ch02.averageFlux U ((a.subSkew g hg).transpose.coeffOn U) (centeredAdjointOptimizer U (a.subSkew g hg) p q) i ∂P) = centeredAdjointResponse P U p (q + matVecMul g p)

A constant-skew recentering preserves the centered adjoint response after the oppositely signed load correction.