High-contrast homogenization: Provider.Response.DiagonalWeakNormAdjointCarriers

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

Adjoint invariance of the diagonal weak carriers

Coefficient transposition and the matching signed reference block leave the maximum and recent defects unchanged. The primal load becomes the adjoint load, while the diagonal metric is fixed.

theorem HCPolySupport.HighContrast.Response.adjointSign_diagonalMetric {d : ℕ} (m : Mat d) : Book.Ch02.blockMatMul (Book.Ch02.blockDiag 1 (-1)) (Book.Ch02.blockMatMul (Book.Ch02.blockDiag m m⁻¹) (Book.Ch02.blockDiag 1 (-1))) = Book.Ch02.blockDiag m m⁻¹

theorem HCPolySupport.HighContrast.Response.adjointSign_blockIdentity {d : ℕ} : Book.Ch02.blockMatMul (Book.Ch02.blockDiag 1 (-1)) (Book.Ch02.blockMatMul (Book.Ch02.blockIdentity d) (Book.Ch02.blockDiag 1 (-1))) = Book.Ch02.blockIdentity d

theorem HCPolySupport.HighContrast.Response.diagonalWeakMetricFactor_adjoint {d : ℕ} (m : Mat d) (E : BlockMat d) : diagonalWeakMetricFactor m (Book.Ch02.blockMatMul (Book.Ch02.blockDiag 1 (-1)) (Book.Ch02.blockMatMul E (Book.Ch02.blockDiag 1 (-1)))) = diagonalWeakMetricFactor m E

theorem HCPolySupport.HighContrast.Response.diagonalWeakLoadMinus_adjoint {d : ℕ} (E : BlockMat d) (p r : Vec d) : diagonalWeakLoadMinus (Book.Ch02.blockMatMul (Book.Ch02.blockDiag 1 (-1)) (Book.Ch02.blockMatMul E (Book.Ch02.blockDiag 1 (-1)))) p r = diagonalWeakLoadPlus E p r

theorem HCPolySupport.HighContrast.Response.diagonalWeakMaximum_adjoint {d : ℕ} (rho : ℝ) {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (E : BlockMat d) (a : CoeffSpace d) : diagonalWeakMaximum rho q t (Book.Ch02.blockMatMul (Book.Ch02.blockDiag 1 (-1)) (Book.Ch02.blockMatMul E (Book.Ch02.blockDiag 1 (-1)))) a.transpose = diagonalWeakMaximum rho q t E a

theorem HCPolySupport.HighContrast.Response.diagonalWeakCellDefect_adjoint {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (k t : ℤ) (E : BlockMat d) (a : CoeffSpace d) : diagonalWeakCellDefect q k t (Book.Ch02.blockMatMul (Book.Ch02.blockDiag 1 (-1)) (Book.Ch02.blockMatMul E (Book.Ch02.blockDiag 1 (-1)))) a.transpose = diagonalWeakCellDefect q k t E a

theorem HCPolySupport.HighContrast.Response.diagonalWeakAverageDefect_adjoint {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (k t : ℤ) {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) (a : CoeffSpace d) : diagonalWeakAverageDefect q k t (Book.Ch02.blockMatMul (Book.Ch02.blockDiag 1 (-1)) (Book.Ch02.blockMatMul E (Book.Ch02.blockDiag 1 (-1)))) a.transpose = Book.Ch02.blockMatMul (Book.Ch02.blockDiag 1 (-1)) (Book.Ch02.blockMatMul (diagonalWeakAverageDefect q k t E a) (Book.Ch02.blockDiag 1 (-1)))

theorem HCPolySupport.HighContrast.Response.blockSize_diagonalWeakAverageDefect_adjoint {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (k t : ℤ) {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) (a : CoeffSpace d) : blockSize (diagonalWeakAverageDefect q k t (Book.Ch02.blockMatMul (Book.Ch02.blockDiag 1 (-1)) (Book.Ch02.blockMatMul E (Book.Ch02.blockDiag 1 (-1)))) a.transpose) (Book.Ch02.blockIdentity d) = blockSize (diagonalWeakAverageDefect q k t E a) (Book.Ch02.blockIdentity d)

theorem HCPolySupport.HighContrast.Response.diagonalWeakCellSum_adjoint {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (H : ℕ) (s : ℝ) (E : BlockMat d) (a : CoeffSpace d) : diagonalWeakCellSum q t H s (Book.Ch02.blockMatMul (Book.Ch02.blockDiag 1 (-1)) (Book.Ch02.blockMatMul E (Book.Ch02.blockDiag 1 (-1)))) a.transpose = diagonalWeakCellSum q t H s E a

theorem HCPolySupport.HighContrast.Response.diagonalWeakAverageSum_adjoint {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (H : ℕ) (s rho : ℝ) {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) (a : CoeffSpace d) : diagonalWeakAverageSum q t H s rho (Book.Ch02.blockMatMul (Book.Ch02.blockDiag 1 (-1)) (Book.Ch02.blockMatMul E (Book.Ch02.blockDiag 1 (-1)))) a.transpose = diagonalWeakAverageSum q t H s rho E a