Documentation

LeanPool.HighContrastHomogenization.Support.Internal.Ch02.Quadraticity

Coarse-graining support: Support.Internal.Ch02.Quadraticity #

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

source
theorem HCPolySupport.Internal.Ch02.BookCh02.responseJ_smul_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 : Vec d) :
Book.Ch02.responseJ U a (c • p) (c • q) = c ^ 2 * Book.Ch02.responseJ U a p q
source
theorem HCPolySupport.Internal.Ch02.BookCh02.responseJ_parallelogram_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) :
Book.Ch02.responseJ U a (p1 + p2) (q1 + q2) + Book.Ch02.responseJ U a (p1 - p2) (q1 - q2) = 2 * Book.Ch02.responseJ U a p1 q1 + 2 * Book.Ch02.responseJ U a p2 q2
source
theorem HCPolySupport.Internal.Ch02.BookCh02.responseQuadraticTheory_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.ResponseQuadraticTheory U a

Internal pointwise-coefficient quadraticity theorem.

source
theorem HCPolySupport.Internal.Ch02.BookCh02.responseQuadraticTheory {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) :
Book.Ch02.ResponseQuadraticTheory U a

Note-facing Chapter 2 quadraticity from the public a.e. coefficient interface. No public pointwise representative or integrability package is exposed.