Coarse-graining support: Support.Book.Ch02.Theorems.MatrixPositivity

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

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

The pure-flux coarse matrix sigmaStarInv(U; a) is positive definite.

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

The derived coarse matrix sigmaStar(U; a) is positive definite.

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

The canonical pure-flux matrix is invertible.

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

The canonical sigmaStar matrix is invertible.

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

The response functional is nonnegative.

theorem HCPolySupport.Book.Ch02.responseJ_zero_right_pos {d : ℕ} (U : Domain d) (a : CoeffOn U) {q : Vec d} (hq : q ≠ 0) : 0 < responseJ U a 0 q

Strict positivity of the pure-flux response away from q = 0.