Coarse-graining support: Support.Internal.Ch02.DoubledResponse.FirstVariation

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

Doubled Response First Variation

This file is split mechanically out of Internal.Ch02.DoubledResponse.

theorem HCPolySupport.Internal.Ch02.BookCh02.first_variation_scalar_representatives_of_isEllipticFieldOn {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (hEll : IsEllipticFieldOn a.lam a.Lam U.carrier a.toCoeffField) (p pStar q qStar : Vec d) (v : Book.Ch02.Solution U a) (vStar : Book.Ch02.Solution U a.transpose) (hv : Book.Ch02.IsResponseMaximizer U a (p - pStar) (qStar - q) v) (hvStar : Book.Ch02.IsResponseMaximizer U a.transpose (pStar + p) (qStar + q) vStar) (w : Book.Ch02.Solution U a) (z : Book.Ch02.Solution U a.transpose) : Book.Ch02.average U (doubledResponseFirstVariationLeft U a (p, q) (qStar, pStar) (Book.Ch02.doubledFieldOfSolutions a w z)) = Book.Ch02.average U (doubledResponseFirstVariationRight U a (Book.Ch02.doubledFieldOfScalarMaximizers a v vStar) (Book.Ch02.doubledFieldOfSolutions a w z))

theorem HCPolySupport.Internal.Ch02.BookCh02.first_variation_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 : BlockVec d) (S T : Book.Ch02.DoubledField d) : Book.Ch02.IsDoubledResponseMaximizer U a P Q S → Book.Ch02.IsDoubledResponseField U a T → (Book.Ch02.average U fun (x : Vec d) => blockVecDot Q (T.eval x) - blockVecDot P (blockMatVecMul (Book.Ch02.blockMatrixField a x) (T.eval x))) = Book.Ch02.average U fun (x : Vec d) => blockVecDot (T.eval x) (blockMatVecMul (Book.Ch02.blockMatrixField a x) (S.eval x))