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

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

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

Public Chapter 2 response-maximizer existence theorem.

The proof is supplied by the internal a.e.-representative bridge, so the public surface only mentions the note-facing Domain and CoeffOn data.

theorem HCPolySupport.Book.Ch02.responseMaximizerExists {d : ℕ} (U : Domain d) (a : CoeffOn U) (p q : Vec d) : ResponseMaximizerExists U a p q

Public per-loading response-maximizer existence, derived from the proved Chapter 2 existence theorem.