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

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

theorem HCPolySupport.Book.Ch02.canonicalResponseMatrixIdentities {d : ℕ} (U : Domain d) (a : CoeffOn U) : CanonicalResponseMatrixIdentities U a

The canonical coarse matrices extracted from the response functional satisfy the note-facing matrix identities.

theorem HCPolySupport.Book.Ch02.responseMatrixExists {d : ℕ} (U : Domain d) (a : CoeffOn U) : ResponseMatrixExists U a

Existence form of matrix extraction, obtained from the canonical matrices.

theorem HCPolySupport.Book.Ch02.responseJ_zero_q_eq_sigmaStarInvCoarse {d : ℕ} (U : Domain d) (a : CoeffOn U) (q : Vec d) : responseJ U a 0 q = 1 / 2 * vecDot q (matVecMul (sigmaStarInvCoarse U a) q)

Public pure-flux quadratic formula defining sigmaStarInv(U; a).

theorem HCPolySupport.Book.Ch02.mixedResponse_eq_sigmaStarInv_kappa {d : ℕ} (U : Domain d) (a : CoeffOn U) (p q : Vec d) : mixedResponse U a p q = vecDot q (matVecMul (sigmaStarInvCoarse U a) (matVecMul (kappaCoarse U a) p))

Public mixed-response formula defining kappa(U; a).

theorem HCPolySupport.Book.Ch02.canonicalSigmaCorrectedResponse_eq_sigmaCoarse {d : ℕ} (U : Domain d) (a : CoeffOn U) (p : Vec d) : canonicalSigmaCorrectedResponse U a p = 1 / 2 * vecDot p (matVecMul (sigmaCoarse U a) p)

Public corrected pure-gradient formula defining sigma(U; a).

theorem HCPolySupport.Book.Ch02.responseJ_eq_coarseMatrices_formula_canonical {d : ℕ} (U : Domain d) (a : CoeffOn U) (p q : Vec d) : responseJ U a p q = 1 / 2 * vecDot p (matVecMul (sigmaCoarse U a) p) + 1 / 2 * vecDot (q + matVecMul (kappaCoarse U a) p) (matVecMul (sigmaStarInvCoarse U a) (q + matVecMul (kappaCoarse U a) p)) - vecDot p q

Public direct coarse-matrix formula for the response functional.