High-contrast homogenization: Provider.Response.AffineResponseSolution

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

Affine covariance of Chapter 2 responses

The adapted cell is the image of its centered reference cube under the grid matrix. Pulling solutions back by this map transforms gradients by the transpose and fluxes by the inverse. The corresponding dual transformations of the two response loads preserve every normalized variational value.

theorem HCPolySupport.HighContrast.exists_affineResponseSolution {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) {a : Book.Ch02.CoeffOn (Response.adaptedDomain hq t)} {aRef : Book.Ch02.CoeffOn (Book.Ch02.cubeDomain (originCube d t))} (haRef : aRef.toCoeffField = affineCoefficient q ⋯ a.toCoeffField) (u : Book.Ch02.Solution (Response.adaptedDomain hq t) a) : ∃ (uRef : Book.Ch02.Solution (Book.Ch02.cubeDomain (originCube d t)) aRef), (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 physical Chapter 2 solution on an adapted cell pulls back to a solution on the centered reference cube, with its exact transpose-transformed gradient.

theorem HCPolySupport.HighContrast.exists_inverseAffineResponseSolution {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) {a : Book.Ch02.CoeffOn (Response.adaptedDomain hq t)} {aRef : Book.Ch02.CoeffOn (Book.Ch02.cubeDomain (originCube d t))} (haRef : aRef.toCoeffField = affineCoefficient q ⋯ a.toCoeffField) (uRef : Book.Ch02.Solution (Book.Ch02.cubeDomain (originCube d t)) aRef) : ∃ (u : Book.Ch02.Solution (Response.adaptedDomain hq t) a), (u.toH1.toFun = fun (x : Vec d) => uRef.toH1.toFun (matVecMul q⁻¹ x)) ∧ u.toH1.grad = fun (x : Vec d) => matVecMul (matTranspose q⁻¹) (uRef.toH1.grad (matVecMul q⁻¹ x))

Every reference-cube solution is the pullback of an adapted-cell solution; the inverse construction records the inverse-transpose gradient explicitly.

theorem HCPolySupport.HighContrast.responseValue_affineResponseSolution {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) {a : Book.Ch02.CoeffOn (Response.adaptedDomain hq t)} {aRef : Book.Ch02.CoeffOn (Book.Ch02.cubeDomain (originCube d t))} (haRef : aRef.toCoeffField = affineCoefficient q ⋯ a.toCoeffField) (p r : Vec d) (u : Book.Ch02.Solution (Response.adaptedDomain hq t) a) (uRef : Book.Ch02.Solution (Book.Ch02.cubeDomain (originCube d t)) aRef) (hgrad : uRef.toH1.grad = fun (y : Vec d) => matVecMul (matTranspose q) (u.toH1.grad (matVecMul q y))) : Book.Ch02.responseValue (Book.Ch02.cubeDomain (originCube d t)) aRef (matVecMul (matTranspose q) p) (matVecMul q⁻¹ r) uRef = Book.Ch02.responseValue (Response.adaptedDomain hq t) a p r u

Response values agree after transforming both loads by the dual affine actions.

theorem HCPolySupport.HighContrast.responseValueSet_affineResponse {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) {a : Book.Ch02.CoeffOn (Response.adaptedDomain hq t)} {aRef : Book.Ch02.CoeffOn (Book.Ch02.cubeDomain (originCube d t))} (haRef : aRef.toCoeffField = affineCoefficient q ⋯ a.toCoeffField) (p r : Vec d) : Book.Ch02.responseValueSet (Book.Ch02.cubeDomain (originCube d t)) aRef (matVecMul (matTranspose q) p) (matVecMul q⁻¹ r) = Book.Ch02.responseValueSet (Response.adaptedDomain hq t) a p r

The physical and reference variational value sets coincide at the dual transformed loads.

theorem HCPolySupport.HighContrast.responseJ_affineResponse {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) {a : Book.Ch02.CoeffOn (Response.adaptedDomain hq t)} {aRef : Book.Ch02.CoeffOn (Book.Ch02.cubeDomain (originCube d t))} (haRef : aRef.toCoeffField = affineCoefficient q ⋯ a.toCoeffField) (p r : Vec d) : Book.Ch02.responseJ (Book.Ch02.cubeDomain (originCube d t)) aRef (matVecMul (matTranspose q) p) (matVecMul q⁻¹ r) = Book.Ch02.responseJ (Response.adaptedDomain hq t) a p r

The Chapter 2 response functional is affine-covariant at the transformed dual loads.