High-contrast homogenization: Provider.Response.DiagonalWeakNormAdjointAlgebra

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

Adjoint sign-congruence algebra

The diagonal sign matrix transports the primal weak estimate to the adjoint coefficient. This file records its involution, order, scalar-size, and inverse-square-root invariances in the doubled block dialect.

theorem HCPolySupport.HighContrast.Response.adjointSign_mulVec {d : ℕ} (X : BlockVec d) : blockMatVecMul (Book.Ch02.blockDiag 1 (-1)) X = (X.1, -X.2)

theorem HCPolySupport.HighContrast.Response.adjointSign_mulVec_involution {d : ℕ} (X : BlockVec d) : blockMatVecMul (Book.Ch02.blockDiag 1 (-1)) (blockMatVecMul (Book.Ch02.blockDiag 1 (-1)) X) = X

theorem HCPolySupport.HighContrast.Response.blockMatVecMul_adjointSign_congr {d : ℕ} (A : BlockMat d) (X : BlockVec d) : blockMatVecMul (Book.Ch02.blockMatMul (Book.Ch02.blockDiag 1 (-1)) (Book.Ch02.blockMatMul A (Book.Ch02.blockDiag 1 (-1)))) X = blockMatVecMul (Book.Ch02.blockDiag 1 (-1)) (blockMatVecMul A (blockMatVecMul (Book.Ch02.blockDiag 1 (-1)) X))

theorem HCPolySupport.HighContrast.Response.blockQuadratic_adjointSign_congr {d : ℕ} (A : BlockMat d) (X : BlockVec d) : blockVecDot X (blockMatVecMul (Book.Ch02.blockMatMul (Book.Ch02.blockDiag 1 (-1)) (Book.Ch02.blockMatMul A (Book.Ch02.blockDiag 1 (-1)))) X) = blockVecDot (blockMatVecMul (Book.Ch02.blockDiag 1 (-1)) X) (blockMatVecMul A (blockMatVecMul (Book.Ch02.blockDiag 1 (-1)) X))

theorem HCPolySupport.HighContrast.Response.adjointSign_mulVec_injective {d : ℕ} (X : BlockVec d) (hX : blockMatVecMul (Book.Ch02.blockDiag 1 (-1)) X = 0) : X = 0

theorem HCPolySupport.HighContrast.Response.adjointSign_congr_loewner_iff {d : ℕ} (A B : BlockMat d) : BlockMatLoewnerLE (Book.Ch02.blockMatMul (Book.Ch02.blockDiag 1 (-1)) (Book.Ch02.blockMatMul A (Book.Ch02.blockDiag 1 (-1)))) (Book.Ch02.blockMatMul (Book.Ch02.blockDiag 1 (-1)) (Book.Ch02.blockMatMul B (Book.Ch02.blockDiag 1 (-1)))) ↔ BlockMatLoewnerLE A B

theorem HCPolySupport.HighContrast.Response.blockScale_adjointSign_congr {d : ℕ} (c : ℝ) (A : BlockMat d) : Book.Ch02.blockMatMul (Book.Ch02.blockDiag 1 (-1)) (Book.Ch02.blockMatMul (blockScale c A) (Book.Ch02.blockDiag 1 (-1))) = blockScale c (Book.Ch02.blockMatMul (Book.Ch02.blockDiag 1 (-1)) (Book.Ch02.blockMatMul A (Book.Ch02.blockDiag 1 (-1))))

theorem HCPolySupport.HighContrast.Response.blockSub_adjointSign_congr {d : ℕ} (A B : BlockMat d) : Book.Ch02.blockMatMul (Book.Ch02.blockDiag 1 (-1)) (Book.Ch02.blockMatMul (blockSub A B) (Book.Ch02.blockDiag 1 (-1))) = blockSub (Book.Ch02.blockMatMul (Book.Ch02.blockDiag 1 (-1)) (Book.Ch02.blockMatMul A (Book.Ch02.blockDiag 1 (-1)))) (Book.Ch02.blockMatMul (Book.Ch02.blockDiag 1 (-1)) (Book.Ch02.blockMatMul B (Book.Ch02.blockDiag 1 (-1))))

theorem HCPolySupport.HighContrast.Response.blockSize_adjointSign_congr {d : ℕ} (A E : BlockMat d) : blockSize (Book.Ch02.blockMatMul (Book.Ch02.blockDiag 1 (-1)) (Book.Ch02.blockMatMul A (Book.Ch02.blockDiag 1 (-1)))) (Book.Ch02.blockMatMul (Book.Ch02.blockDiag 1 (-1)) (Book.Ch02.blockMatMul E (Book.Ch02.blockDiag 1 (-1)))) = blockSize A E

theorem HCPolySupport.HighContrast.Response.blockExcess_adjointSign_congr {d : ℕ} (A E : BlockMat d) : blockExcess (Book.Ch02.blockMatMul (Book.Ch02.blockDiag 1 (-1)) (Book.Ch02.blockMatMul A (Book.Ch02.blockDiag 1 (-1)))) (Book.Ch02.blockMatMul (Book.Ch02.blockDiag 1 (-1)) (Book.Ch02.blockMatMul E (Book.Ch02.blockDiag 1 (-1)))) = blockExcess A E

theorem HCPolySupport.HighContrast.Response.blockPosDef_adjointSign_congr {d : ℕ} {A : BlockMat d} (hA : Book.Ch02.BlockPosDef A) : Book.Ch02.BlockPosDef (Book.Ch02.blockMatMul (Book.Ch02.blockDiag 1 (-1)) (Book.Ch02.blockMatMul A (Book.Ch02.blockDiag 1 (-1))))

theorem HCPolySupport.HighContrast.Response.isSymmetricBlockMat_adjointSign_congr {d : ℕ} {A : BlockMat d} (hA : IsSymmetricBlockMat A) : IsSymmetricBlockMat (Book.Ch02.blockMatMul (Book.Ch02.blockDiag 1 (-1)) (Book.Ch02.blockMatMul A (Book.Ch02.blockDiag 1 (-1))))

theorem HCPolySupport.HighContrast.Response.adjointSign_mul_self {d : ℕ} : toFullBlockMat (Book.Ch02.blockDiag 1 (-1)) * toFullBlockMat (Book.Ch02.blockDiag 1 (-1)) = 1

theorem HCPolySupport.HighContrast.Response.adjointSign_conjTranspose {d : ℕ} : Matrix.conjTranspose (toFullBlockMat (Book.Ch02.blockDiag 1 (-1))) = toFullBlockMat (Book.Ch02.blockDiag 1 (-1))

theorem HCPolySupport.HighContrast.Response.isUnit_adjointSign {d : ℕ} : IsUnit (toFullBlockMat (Book.Ch02.blockDiag 1 (-1)))

theorem HCPolySupport.HighContrast.Response.adjointSign_inv {d : ℕ} : (toFullBlockMat (Book.Ch02.blockDiag 1 (-1)))⁻¹ = toFullBlockMat (Book.Ch02.blockDiag 1 (-1))

theorem HCPolySupport.HighContrast.Response.adjointSign_congr_inv {d : ℕ} (E : BlockMat d) : (toFullBlockMat (Book.Ch02.blockDiag 1 (-1)) * toFullBlockMat E * toFullBlockMat (Book.Ch02.blockDiag 1 (-1)))⁻¹ = toFullBlockMat (Book.Ch02.blockDiag 1 (-1)) * (toFullBlockMat E)⁻¹ * toFullBlockMat (Book.Ch02.blockDiag 1 (-1))

theorem HCPolySupport.HighContrast.Response.adjointSign_congr_sqrt_inv {d : ℕ} {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) : matSqrt (toFullBlockMat (Book.Ch02.blockDiag 1 (-1)) * (toFullBlockMat E * toFullBlockMat (Book.Ch02.blockDiag 1 (-1))))⁻¹ = toFullBlockMat (Book.Ch02.blockDiag 1 (-1)) * (matSqrt (toFullBlockMat E)⁻¹ * toFullBlockMat (Book.Ch02.blockDiag 1 (-1)))

theorem HCPolySupport.HighContrast.Response.normalizedBlock_adjointSign_congr {d : ℕ} {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) (A : BlockMat d) : normalizedBlock (Book.Ch02.blockMatMul (Book.Ch02.blockDiag 1 (-1)) (Book.Ch02.blockMatMul A (Book.Ch02.blockDiag 1 (-1)))) (Book.Ch02.blockMatMul (Book.Ch02.blockDiag 1 (-1)) (Book.Ch02.blockMatMul E (Book.Ch02.blockDiag 1 (-1)))) = Book.Ch02.blockMatMul (Book.Ch02.blockDiag 1 (-1)) (Book.Ch02.blockMatMul (normalizedBlock A E) (Book.Ch02.blockDiag 1 (-1)))