Coarse-graining support: Support.Internal.Ch02.DoubledResponse.Theory #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Doubled Response Theory Assembly #
This file is split mechanically out of Internal.Ch02.DoubledResponse.
theorem
HCPolySupport.Internal.Ch02.BookCh02.doubledResponseTheory_of_isEllipticFieldOn
{d : ℕ}
(U : Book.Ch02.Domain d)
(a : Book.Ch02.CoeffOn U)
(hEll : IsEllipticFieldOn a.lam a.Lam U.carrier a.toCoeffField)
:
theorem
HCPolySupport.Internal.Ch02.BookCh02.doubledResponseTheory_ofAEEq
{d : ℕ}
{U : Book.Ch02.Domain d}
{a b : Book.Ch02.CoeffOn U}
(h : a.AEEq b)
(ha : Book.Ch02.DoubledResponseTheory U a)
:
theorem
HCPolySupport.Internal.Ch02.BookCh02.doubledResponseTheory
{d : ℕ}
(U : Book.Ch02.Domain d)
(a : Book.Ch02.CoeffOn U)
: