High-contrast homogenization: Provider.Response.CenteredResponseAdjointAnnealed

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

Annealed adjoint response identities

Coefficient transposition conjugates every coarse block by the diagonal sign matrix. Integrating that pointwise congruence identifies the adjoint response energy and both adjoint optimizer means with the same congruence of the annealed primal block.

theorem HCPolySupport.HighContrast.Response.adjoint_coarseBlock_mulVec_eq {d : ℕ} (U : Book.Ch02.Domain d) (a : CoeffSpace d) (X : BlockVec d) : blockMatVecMul (coarseBlock U.carrier a.transpose) X = blockMatVecMul (Book.Ch02.blockDiag 1 (-1)) (blockMatVecMul (coarseBlock U.carrier a) (blockMatVecMul (Book.Ch02.blockDiag 1 (-1)) X))

Applying an adjoint coarse block is the signed transport of applying the original coarse block.

theorem HCPolySupport.HighContrast.Response.integrable_adjoint_coarseBlock_mulVec_apply {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} (U : Book.Ch02.Domain d) (hint : HasIntegrableCoarseBlock P U.carrier) (X : BlockVec d) (α : BlockCoord d) : MeasureTheory.Integrable (fun (a : CoeffSpace d) => toFullBlockVec (blockMatVecMul (coarseBlock U.carrier a.transpose) X) α) P

Each coordinate of an adjoint coarse block applied to a fixed vector is integrable under integrability of the primal coarse block.

theorem HCPolySupport.HighContrast.Response.integral_adjoint_coarseBlock_mulVec {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} (U : Book.Ch02.Domain d) (hint : HasIntegrableCoarseBlock P U.carrier) (X : BlockVec d) : (fun (α : BlockCoord d) => ∫ (a : CoeffSpace d), toFullBlockVec (blockMatVecMul (coarseBlock U.carrier a.transpose) X) α ∂P) = toFullBlockVec (blockMatVecMul (Book.Ch02.blockMatMul (Book.Ch02.blockDiag 1 (-1)) (Book.Ch02.blockMatMul (annealedBlock P U.carrier) (Book.Ch02.blockDiag 1 (-1)))) X)

Integration commutes with applying the adjoint coarse block; the result is the sign congruence of the annealed primal block.

theorem HCPolySupport.HighContrast.Response.integral_adjoint_coarseBlock_quadratic {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} (U : Book.Ch02.Domain d) (hint : HasIntegrableCoarseBlock P U.carrier) (X : BlockVec d) : ∫ (a : CoeffSpace d), blockVecDot X (blockMatVecMul (coarseBlock U.carrier a.transpose) X) ∂P = blockVecDot X (blockMatVecMul (Book.Ch02.blockMatMul (Book.Ch02.blockDiag 1 (-1)) (Book.Ch02.blockMatMul (annealedBlock P U.carrier) (Book.Ch02.blockDiag 1 (-1)))) X)

The expected adjoint quadratic form is the quadratic form of the signed congruence of the annealed block.

theorem HCPolySupport.HighContrast.Response.annealed_adjoint_responseJ_eq {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (U : Book.Ch02.Domain d) (hint : HasIntegrableCoarseBlock P U.carrier) (p q : Vec d) : ∫ (a : CoeffSpace d), Book.Ch02.responseJ U (a.transpose.coeffOn U) p q ∂P = 1 / 2 * blockVecDot (-p, q) (blockMatVecMul (Book.Ch02.blockMatMul (Book.Ch02.blockDiag 1 (-1)) (Book.Ch02.blockMatMul (annealedBlock P U.carrier) (Book.Ch02.blockDiag 1 (-1)))) (-p, q)) - vecDot p q

The annealed adjoint response energy is the quadratic form of the signed annealed block.

theorem HCPolySupport.HighContrast.Response.annealed_adjoint_optimizer_average_eq {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (U : Book.Ch02.Domain d) (hint : HasIntegrableCoarseBlock P U.carrier) (p q : Vec d) : (annealedAdjointOptimizerGradient P U p q, annealedAdjointOptimizerFlux P U p q) = blockMatVecMul (Book.Ch02.blockR d) (blockMatVecMul (Book.Ch02.blockMatMul (Book.Ch02.blockDiag 1 (-1)) (Book.Ch02.blockMatMul (annealedBlock P U.carrier) (Book.Ch02.blockDiag 1 (-1)))) (-p, q)) + (-p, q)

The separately annealed adjoint optimizer averages are read from the two rows of the signed annealed block.