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

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

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

Public Chapter 2 doubled-response theorem package for l.block.response.functional.basic.definitions.

The coefficient field is used through the a.e. public CoeffOn interface; no pointwise ellipticity or representative choice is exposed.