Documentation

LeanPool.HighContrastHomogenization.Support.Internal.Ch02.GradientUniqueness

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

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

source
theorem HCPolySupport.Internal.Ch02.BookCh02.responseGradientUniquenessTheory_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.ResponseGradientUniquenessTheory U a

Internal pointwise-coefficient gradient uniqueness theorem.

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

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