Documentation

LeanPool.HighContrastHomogenization.Provider.Response.AffineResponseCoefficient

High-contrast homogenization: Provider.Response.AffineResponseCoefficient #

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

Reference-cube coefficients for an adapted response #

A coefficient from the physical coefficient space is globally measurable and locally uniformly elliptic. Pulling it back by the adapted grid gives a compatible coefficient family on all reference cubes and, in particular, a coefficient object on the centered cube corresponding to the physical adapted domain.

source
theorem HCPolySupport.HighContrast.exists_adaptedReferenceCoeffFamily {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (a : CoeffSpace d) :
∃ (aRef : Book.Ch03.CoeffFamily d), ∀ (Q : TriadicCube d), (aRef.coeffOn Q).toCoeffField = affineCoefficient q ⋯ (a.coeffOn (Response.adaptedDomain hq t)).toCoeffField

An adapted physical coefficient produces one compatible affine-pullback coefficient family on the reference triadic cubes.

source
theorem HCPolySupport.HighContrast.exists_adaptedReferenceCoeffOn {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (a : CoeffSpace d) :
∃ (aRef : Book.Ch02.CoeffOn (Book.Ch02.cubeDomain (originCube d t))), aRef.toCoeffField = affineCoefficient q ⋯ (a.coeffOn (Response.adaptedDomain hq t)).toCoeffField

The compatible affine family supplies the coefficient object on the centered reference cube associated with an adapted response domain.