Coarse-graining support: Support.CoarseGraining.BlockFormalism.MatrixIdentities

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Block formalism -- matrix identities and conjugation

blockMatrixOfCoeff matTranspose / primal / adjoint identities, blockVecDot / blockMatVecMul conj-by-involution lemmas, signFlip and swap conjugation identities, and the blockMatrixOfCoeff_quadratic_eq / matTranspose_flipFlux identities.

@[simp]

theorem HCPolySupport.blockMatrixOfCoeff_matTranspose_lowerRight {d : ℕ} (A : Mat d) : (blockMatrixOfCoeff (matTranspose A)).lowerRight = (blockMatrixOfCoeff A).lowerRight

theorem HCPolySupport.blockMatrixOfCoeff_matTranspose {d : ℕ} (A : Mat d) : blockMatrixOfCoeff (matTranspose A) = { upperLeft := (blockMatrixOfCoeff A).upperLeft, upperRight := -(blockMatrixOfCoeff A).upperRight, lowerLeft := -(blockMatrixOfCoeff A).lowerLeft, lowerRight := (blockMatrixOfCoeff A).lowerRight }

theorem HCPolySupport.blockMatVecMul_blockMatrixOfCoeff_snd {d : ℕ} (A : Mat d) (p q : Vec d) : (blockMatVecMul (blockMatrixOfCoeff A) (p, q)).2 = matVecMul (symmPart A)⁻¹ (q - matVecMul (skewPart A) p)

theorem HCPolySupport.blockMatVecMul_blockMatrixOfCoeff_fst {d : ℕ} (A : Mat d) (p q : Vec d) : (blockMatVecMul (blockMatrixOfCoeff A) (p, q)).1 = matVecMul (symmPart A) p + matVecMul (skewPart A) (matVecMul (symmPart A)⁻¹ (q - matVecMul (skewPart A) p))

theorem HCPolySupport.blockMatVecMul_blockMatrixOfCoeff_primal_of_isUnit_det_symmPart {d : ℕ} (A : Mat d) (hdet : IsUnit (Matrix.det (symmPart A))) (ξ : Vec d) : blockMatVecMul (blockMatrixOfCoeff A) (ξ, matVecMul A ξ) = (matVecMul A ξ, ξ)

theorem HCPolySupport.blockMatVecMul_blockMatrixOfCoeff_adjoint_of_isUnit_det_symmPart {d : ℕ} (A : Mat d) (hdet : IsUnit (Matrix.det (symmPart A))) (η : Vec d) : blockMatVecMul (blockMatrixOfCoeff A) (η, -matVecMul (matTranspose A) η) = (matVecMul (matTranspose A) η, -η)

theorem HCPolySupport.blockMatVecMul_blockMatrixOfCoeff_primal_of_isEllipticMatrix {d : ℕ} {lam Lam : ℝ} {A : Mat d} (hA : IsEllipticMatrix lam Lam A) (ξ : Vec d) : blockMatVecMul (blockMatrixOfCoeff A) (ξ, matVecMul A ξ) = (matVecMul A ξ, ξ)

theorem HCPolySupport.blockMatVecMul_blockMatrixOfCoeff_adjoint_of_isEllipticMatrix {d : ℕ} {lam Lam : ℝ} {A : Mat d} (hA : IsEllipticMatrix lam Lam A) (η : Vec d) : blockMatVecMul (blockMatrixOfCoeff A) (η, -matVecMul (matTranspose A) η) = (matVecMul (matTranspose A) η, -η)

theorem HCPolySupport.blockVecDot_blockVecConj_of_transpose_eq_self_of_mul_self_eq_one {d : ℕ} {R : Mat d} (hR : matTranspose R = R) (hR2 : R * R = 1) (X Y : BlockVec d) : blockVecDot (blockVecConj R X) (blockVecConj R Y) = blockVecDot X Y

theorem HCPolySupport.blockMatVecMul_blockMatConj_of_mul_self_eq_one {d : ℕ} {R : Mat d} (hR2 : R * R = 1) (B : BlockMat d) (X : BlockVec d) : blockMatVecMul (blockMatConj R B) (blockVecConj R X) = blockVecConj R (blockMatVecMul B X)

theorem HCPolySupport.blockMatrixOfCoeff_conj_of_transpose_eq_self_of_mul_self_eq_one {d : ℕ} {R A : Mat d} (hR : matTranspose R = R) (hR2 : R * R = 1) : blockMatrixOfCoeff (R * A * R) = blockMatConj R (blockMatrixOfCoeff A)

theorem HCPolySupport.matTranspose_signFlipMatrix {d : ℕ} (i : Fin d) : matTranspose (signFlipMatrix i) = signFlipMatrix i

theorem HCPolySupport.signFlipMatrix_mul_self {d : ℕ} (i : Fin d) : signFlipMatrix i * signFlipMatrix i = 1

theorem HCPolySupport.blockMatrixOfCoeff_signFlipMatrix_conj {d : ℕ} (i : Fin d) (A : Mat d) : blockMatrixOfCoeff (signFlipMatrix i * A * signFlipMatrix i) = blockMatConj (signFlipMatrix i) (blockMatrixOfCoeff A)

theorem HCPolySupport.blockMatrixOfCoeff_swap_conj {d : ℕ} (i j : Fin d) (A : Mat d) : blockMatrixOfCoeff (Matrix.swap ℝ i j * A * Matrix.swap ℝ i j) = blockMatConj (Matrix.swap ℝ i j) (blockMatrixOfCoeff A)

theorem HCPolySupport.blockMatrixOfCoeff_quadratic_eq {d : ℕ} (A : Mat d) (p q : Vec d) : blockVecDot (p, q) (blockMatVecMul (blockMatrixOfCoeff A) (p, q)) = vecDot p (matVecMul (symmPart A) p) + vecDot (q - matVecMul (skewPart A) p) (matVecMul (symmPart A)⁻¹ (q - matVecMul (skewPart A) p))

theorem HCPolySupport.blockMatrixOfCoeff_quadratic_matTranspose_flipFlux {d : ℕ} (A : Mat d) (p q : Vec d) : blockVecDot (p, -q) (blockMatVecMul (blockMatrixOfCoeff (matTranspose A)) (p, -q)) = blockVecDot (p, q) (blockMatVecMul (blockMatrixOfCoeff A) (p, q))

theorem HCPolySupport.blockVecDot_blockMatVecMul_blockMatrixOfCoeff_conj_of_transpose_eq_self_of_mul_self_eq_one {d : ℕ} {R A : Mat d} (hR : matTranspose R = R) (hR2 : R * R = 1) (X : BlockVec d) : blockVecDot (blockVecConj R X) (blockMatVecMul (blockMatrixOfCoeff (R * A * R)) (blockVecConj R X)) = blockVecDot X (blockMatVecMul (blockMatrixOfCoeff A) X)