High-contrast homogenization: Provider.Response.AffineResponseCell #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Affine covariance on aligned response cells #
Every aligned adapted cell is the grid image of the correspondingly translated reference cube. A single compatible reference coefficient family therefore transports the Chapter 2 solutions, response values, and second variations on all cells of an aligned subdivision.
theorem
HCPolySupport.HighContrast.exists_affineResponseCellSolution
{d : ℕ}
{q : Mat d}
(hq : Matrix.PosDef q)
(t k : ℤ)
(w : Fin d → ℤ)
(a : CoeffSpace d)
(aRef : Book.Ch03.CoeffFamily d)
(haRef :
∀ (Q : TriadicCube d),
(aRef.coeffOn Q).toCoeffField = affineCoefficient q ⋯ (a.coeffOn (Response.adaptedDomain hq t)).toCoeffField)
(u : Book.Ch02.Solution (Response.adaptedDomainAt hq k w) (a.coeffOn (Response.adaptedDomainAt hq k w)))
:
∃ (uRef :
Book.Ch02.Solution (Book.Ch02.cubeDomain (translateCube w (originCube d k)))
(aRef.coeffOn (translateCube w (originCube d k)))),
(uRef.toH1.toFun = fun (y : Vec d) => u.toH1.toFun (matVecMul q y)) ∧ uRef.toH1.grad = fun (y : Vec d) => matVecMul (matTranspose q) (u.toH1.grad (matVecMul q y))
A solution on an aligned adapted cell pulls back to the matching translated reference cube using the same compatible reference coefficient family as the parent cell.
theorem
HCPolySupport.HighContrast.responseJ_affineResponseCell
{d : ℕ}
{q : Mat d}
(hq : Matrix.PosDef q)
(t k : ℤ)
(w : Fin d → ℤ)
(a : CoeffSpace d)
(aRef : Book.Ch03.CoeffFamily d)
(haRef :
∀ (Q : TriadicCube d),
(aRef.coeffOn Q).toCoeffField = affineCoefficient q ⋯ (a.coeffOn (Response.adaptedDomain hq t)).toCoeffField)
(p r : Vec d)
:
Book.Ch02.responseJ (Book.Ch02.cubeDomain (translateCube w (originCube d k)))
(aRef.coeffOn (translateCube w (originCube d k))) (matVecMul (matTranspose q) p) (matVecMul q⁻¹ r) = Book.Ch02.responseJ (Response.adaptedDomainAt hq k w) (a.coeffOn (Response.adaptedDomainAt hq k w)) p r
The response functional on every aligned physical cell equals the response on its translated reference cube at the dual transformed loads.