Coarse-graining support: Support.Book.Ch02.Theorems.MagicIdentities #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.Book.Ch02.responseMagicIdentitiesTheory
{d : ℕ}
(U : Domain d)
(a : CoeffOn U)
:
Public note-facing magic identities for the response functional.