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

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

theorem HCPolySupport.Internal.Ch02.BookCh02.responseMaximizerExists_of_scalarCanonicalMaximizer {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) {p q : Vec d} (v : ScalarCanonicalMaximizer U.carrier p q a.toCoeffField) : Book.Ch02.ResponseMaximizerExists U a p q

Internal bridge from the old canonical maximizer package to the new public Chapter 2 existence package.

theorem HCPolySupport.Internal.Ch02.BookCh02.responseMaximizerExists_of_isEllipticFieldOn {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (hEll : IsEllipticFieldOn a.lam a.Lam U.carrier a.toCoeffField) (p q : Vec d) : Book.Ch02.ResponseMaximizerExists U a p q

Internal pointwise-coefficient bridge. This is not the final public note-facing theorem: it is the adapter that lets the old Hilbert existence engine feed the new public package whenever an internal representative has already been upgraded to pointwise ellipticity.

theorem HCPolySupport.Internal.Ch02.BookCh02.responseExistenceTheory_of_isEllipticFieldOn {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (hEll : IsEllipticFieldOn a.lam a.Lam U.carrier a.toCoeffField) : Book.Ch02.ResponseExistenceTheory U a

Internal pointwise-coefficient existence theory. The public a.e. theorem is proved below by changing representatives first.

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

Note-facing Chapter 2 response-maximizer existence from the public a.e. coefficient interface. Pointwise ellipticity is used only for the private representative pointwiseCoeffOn U a, and the result is transported back across a.e. equality of coefficient representatives.