Coarse-graining support: Support.Internal.Ch02.BlockCoarseMatrix #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.Internal.Ch02.BookCh02.responseJ_eq_block_quadratic
{d : ℕ}
(U : Book.Ch02.Domain d)
(a : Book.Ch02.CoeffOn U)
(p q : Vec d)
:
Book.Ch02.responseJ U a p q = 1 / 2 * blockVecDot (-p, q) (blockMatVecMul (Book.Ch02.coarseBlockMatrix U a) (-p, q)) - vecDot p q
theorem
HCPolySupport.Internal.Ch02.BookCh02.blockCoarseMatrixTheory
{d : ℕ}
(U : Book.Ch02.Domain d)
(a : Book.Ch02.CoeffOn U)
: