Coarse-graining support: Support.Internal.Ch02.BlockMatrixField

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

theorem HCPolySupport.Internal.Ch02.BookCh02.book_blockMatrixField_eq_blockCoeffField {d : ℕ} {U : Book.Ch02.Domain d} (a : Book.Ch02.CoeffOn U) (x : Vec d) : Book.Ch02.blockMatrixField a x = blockCoeffField a.toCoeffField x

theorem HCPolySupport.Internal.Ch02.BookCh02.book_blockMatrixInverseField_eq_blockReflect {d : ℕ} {U : Book.Ch02.Domain d} (a : Book.Ch02.CoeffOn U) (x : Vec d) : Book.Ch02.blockMatrixInverseField a x = blockReflect (Book.Ch02.blockMatrixField a x)

theorem HCPolySupport.Internal.Ch02.BookCh02.blockMatrixOfCoeff_factorization {d : ℕ} (A : Mat d) : blockMatrixOfCoeff A = Book.Ch02.blockMatMul (Book.Ch02.blockMatTranspose (Book.Ch02.blockG (-skewPart A))) (Book.Ch02.blockMatMul (Book.Ch02.blockDiag (symmPart A) (symmPart A)⁻¹) (Book.Ch02.blockG (-skewPart A)))

theorem HCPolySupport.Internal.Ch02.BookCh02.blockMatrixField_factorization {d : ℕ} {U : Book.Ch02.Domain d} (a : Book.Ch02.CoeffOn U) (x : Vec d) : Book.Ch02.blockMatrixField a x = Book.Ch02.blockMatMul (Book.Ch02.blockMatTranspose (Book.Ch02.blockG (-skewPart (a.toCoeffField x)))) (Book.Ch02.blockMatMul (Book.Ch02.blockDiag (symmPart (a.toCoeffField x)) (symmPart (a.toCoeffField x))⁻¹) (Book.Ch02.blockG (-skewPart (a.toCoeffField x))))

theorem HCPolySupport.Internal.Ch02.BookCh02.blockMatrixFieldAlgebraTheory_of_coeffOn {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) : Book.Ch02.BlockMatrixFieldAlgebraTheory U a

theorem HCPolySupport.Internal.Ch02.BookCh02.blockMatrixFieldAlgebraTheory {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) : Book.Ch02.BlockMatrixFieldAlgebraTheory U a