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

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

theorem HCPolySupport.Internal.Ch02.BookCh02.sigmaStarInvCoarse_posDef_of_isEllipticFieldOn {d : ℕ} [NeZero d] (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (hEll : IsEllipticFieldOn a.lam a.Lam U.carrier a.toCoeffField) : Matrix.PosDef (Book.Ch02.sigmaStarInvCoarse U a)

theorem HCPolySupport.Internal.Ch02.BookCh02.sigmaStarInvCoarse_posDef {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) : Matrix.PosDef (Book.Ch02.sigmaStarInvCoarse U a)

theorem HCPolySupport.Internal.Ch02.BookCh02.sigmaStarCoarse_posDef {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) : Matrix.PosDef (Book.Ch02.sigmaStarCoarse U a)

theorem HCPolySupport.Internal.Ch02.BookCh02.isUnit_det_sigmaStarInvCoarse {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) : IsUnit (Matrix.det (Book.Ch02.sigmaStarInvCoarse U a))

theorem HCPolySupport.Internal.Ch02.BookCh02.isUnit_det_sigmaStarCoarse {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) : IsUnit (Matrix.det (Book.Ch02.sigmaStarCoarse U a))

theorem HCPolySupport.Internal.Ch02.BookCh02.responseJ_nonneg {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (p q : Vec d) : 0 ≤ Book.Ch02.responseJ U a p q