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

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

theorem HCPolySupport.Internal.Ch02.BookCh02.responseCoarseGrainingEstimatesTheory {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) : Book.Ch02.ResponseCoarseGrainingEstimatesTheory U a