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

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

theorem HCPolySupport.Internal.Ch02.BookCh02.addOfIntegrable_isResponseMaximizer_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 : Vec d) (v1 v2 : Book.Ch02.Solution U a) (h1 : Book.Ch02.IsResponseMaximizer U a p1 q1 v1) (h2 : Book.Ch02.IsResponseMaximizer U a p2 q2 v2) : have hInt := ⋯; IsResponseMaximizer U.carrier (p1 + p2) (q1 + q2) a.toCoeffField (AHarmonicFunction.addOfIntegrable v1 v2 ⋯ ⋯)

theorem HCPolySupport.Internal.Ch02.BookCh02.responseGradientLinearityTheory_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.ResponseGradientLinearityTheory U a

Internal pointwise-coefficient gradient-linearity theorem.

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

Note-facing Chapter 2 gradient linearity from the public a.e. coefficient interface.