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

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

Doubled Maximizer Algebra

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

theorem HCPolySupport.Internal.Ch02.BookCh02.doubledFieldOfScalarMaximizers_sameAE_of_sameGradient {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) {v w : Book.Ch02.Solution U a} {vStar wStar : Book.Ch02.Solution U a.transpose} (hvw : v.SameGradientAE w) (hvStarwStar : vStar.SameGradientAE wStar) : (Book.Ch02.doubledFieldOfScalarMaximizers a v vStar).SameAE (Book.Ch02.doubledFieldOfScalarMaximizers a w wStar)

theorem HCPolySupport.Internal.Ch02.BookCh02.doubledFieldOfScalarMaximizers_sameAE_add_of_grad_add {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) {v12 v1 v2 : Book.Ch02.Solution U a} {vStar12 vStar1 vStar2 : Book.Ch02.Solution U a.transpose} (hv : v12.toH1.grad =ᵐ[volumeMeasureOn U.carrier] fun (x : Vec d) => v1.toH1.grad x + v2.toH1.grad x) (hvStar : vStar12.toH1.grad =ᵐ[volumeMeasureOn U.carrier] fun (x : Vec d) => vStar1.toH1.grad x + vStar2.toH1.grad x) : (Book.Ch02.doubledFieldOfScalarMaximizers a v12 vStar12).SameAE (Book.Ch02.doubledFieldOfScalarMaximizers a v1 vStar1 + Book.Ch02.doubledFieldOfScalarMaximizers a v2 vStar2)

theorem HCPolySupport.Internal.Ch02.BookCh02.doubledFieldOfScalarMaximizers_sameAE_smul_of_grad_smul {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (c : ℝ) {vc v : Book.Ch02.Solution U a} {vStarc vStar : Book.Ch02.Solution U a.transpose} (hv : vc.toH1.grad =ᵐ[volumeMeasureOn U.carrier] fun (x : Vec d) => c • v.toH1.grad x) (hvStar : vStarc.toH1.grad =ᵐ[volumeMeasureOn U.carrier] fun (x : Vec d) => c • vStar.toH1.grad x) : (Book.Ch02.doubledFieldOfScalarMaximizers a vc vStarc).SameAE (c • Book.Ch02.doubledFieldOfScalarMaximizers a v vStar)

theorem HCPolySupport.Internal.Ch02.BookCh02.maximizer_unique_ae_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) (X Y : Book.Ch02.DoubledField d) : Book.Ch02.IsDoubledResponseMaximizer U a P Q X → Book.Ch02.IsDoubledResponseMaximizer U a P Q Y → X.SameAE Y

theorem HCPolySupport.Internal.Ch02.BookCh02.maximizer_add_sameAE_of_isEllipticFieldOn {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (hEll : IsEllipticFieldOn a.lam a.Lam U.carrier a.toCoeffField) (P1 Q1 P2 Q2 : BlockVec d) (X12 X1 X2 : Book.Ch02.DoubledField d) : Book.Ch02.IsDoubledResponseMaximizer U a (P1 + P2) (Q1 + Q2) X12 → Book.Ch02.IsDoubledResponseMaximizer U a P1 Q1 X1 → Book.Ch02.IsDoubledResponseMaximizer U a P2 Q2 X2 → X12.SameAE (X1 + X2)

theorem HCPolySupport.Internal.Ch02.BookCh02.maximizer_smul_sameAE_of_isEllipticFieldOn {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (hEll : IsEllipticFieldOn a.lam a.Lam U.carrier a.toCoeffField) (c : ℝ) (P Q : BlockVec d) (Xc X : Book.Ch02.DoubledField d) : Book.Ch02.IsDoubledResponseMaximizer U a (c • P) (c • Q) Xc → Book.Ch02.IsDoubledResponseMaximizer U a P Q X → Xc.SameAE (c • X)