High-contrast homogenization:

Provider.PolynomialHomogenization.Root.RowSupply.LocalDoubledResponseTranslation

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Local translation covariance for doubled responses

The public coefficient carrier is defined only almost everywhere. This file packages translation covariance without selecting pointwise representatives: the coefficient on the translated cube and the translated coefficient on the base cube need only agree almost everywhere with a common physical field.

noncomputable def HCPolySupport.HighContrast.RowSupply.replaceCoeffOn {d : ℕ} {U : Book.Ch02.Domain d} (a : Book.Ch02.CoeffOn U) (f : CoeffField d) (h : f =ᵐ[volumeMeasureOn U.carrier] a.toCoeffField) : Book.Ch02.CoeffOn U

Replace a coefficient representative by an a.e.-equal field on the domain, retaining its ellipticity bounds.

Equations

• HCPolySupport.HighContrast.RowSupply.replaceCoeffOn a f h = { toCoeffField := f, lam := a.lam, Lam := a.Lam, lam_pos := ⋯, lam_le_Lam := ⋯, aeStronglyMeasurable := ⋯, aeElliptic := ⋯ }

theorem HCPolySupport.HighContrast.RowSupply.doubledResponseJ_translate_of_aeeq {d : ℕ} {U V : Book.Ch02.Domain d} (z : Vec d) (hset : U.carrier = translateSet z V.carrier) (aU : Book.Ch02.CoeffOn U) (aV : Book.Ch02.CoeffOn V) (hcoeff : translateCoeffField z aU.toCoeffField =ᵐ[volumeMeasureOn V.carrier] aV.toCoeffField) (P Q : BlockVec d) : Book.Ch02.doubledResponseJ U aU P Q = Book.Ch02.doubledResponseJ V aV P Q

The doubled response is translation covariant under local a.e. identification of the translated coefficient field.