Documentation

LeanPool.HighContrastHomogenization.Support.Internal.Ch02.FirstVariation

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

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

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

Internal pointwise-coefficient first-variation theorem.

This is the proof-engine bridge only. The public theorem below first replaces the public a.e. coefficient by a pointwise-good representative, uses this bridge, and transports the result back across a.e. equality.

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

Note-facing Chapter 2 first variation from the public a.e. coefficient interface. No public pointwise ellipticity, integrability package, or representative choice is exposed.