High-contrast homogenization: Provider.Response.ConstantSkewResponse

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

Constant-skew covariance of the response functional

The harmonic solution spaces for a and a - g have the same gradients when g is constant and skew. On those common gradients, subtracting g from the coefficient is exactly compensated by replacing the second load q with q - g p.

theorem HCPolySupport.HighContrast.Response.exists_solution_subSkew {d : ℕ} {U : Book.Ch02.Domain d} {a b : Book.Ch02.CoeffOn U} (g : Mat d) (hg : IsSkewMat g) (hshift : b.toCoeffField =ᵐ[volumeMeasureOn U.carrier] fun (x : Vec d) => a.toCoeffField x - g) (u : Book.Ch02.Solution U a) : ∃ (v : Book.Ch02.Solution U b), v.toH1 = u.toH1

A solution for a gives a solution with the same H¹ representative for a - g.

theorem HCPolySupport.HighContrast.Response.exists_solution_of_subSkew {d : ℕ} {U : Book.Ch02.Domain d} {a b : Book.Ch02.CoeffOn U} (g : Mat d) (hg : IsSkewMat g) (hshift : b.toCoeffField =ᵐ[volumeMeasureOn U.carrier] fun (x : Vec d) => a.toCoeffField x - g) (v : Book.Ch02.Solution U b) : ∃ (u : Book.Ch02.Solution U a), u.toH1 = v.toH1

Conversely, a solution for a - g gives a solution with the same H¹ representative for a.

theorem HCPolySupport.HighContrast.Response.responseValue_subSkew {d : ℕ} {U : Book.Ch02.Domain d} {a b : Book.Ch02.CoeffOn U} (g : Mat d) (hg : IsSkewMat g) (hshift : b.toCoeffField =ᵐ[volumeMeasureOn U.carrier] fun (x : Vec d) => a.toCoeffField x - g) (p q : Vec d) (u : Book.Ch02.Solution U a) (v : Book.Ch02.Solution U b) (hv : v.toH1 = u.toH1) : Book.Ch02.responseValue U b p q v = Book.Ch02.responseValue U a p (q - matVecMul g p) u

The response value of matching solutions is covariant under a constant skew recentering.

theorem HCPolySupport.HighContrast.Response.responseValueSet_subSkew {d : ℕ} {U : Book.Ch02.Domain d} {a b : Book.Ch02.CoeffOn U} (g : Mat d) (hg : IsSkewMat g) (hshift : b.toCoeffField =ᵐ[volumeMeasureOn U.carrier] fun (x : Vec d) => a.toCoeffField x - g) (p q : Vec d) : Book.Ch02.responseValueSet U b p q = Book.Ch02.responseValueSet U a p (q - matVecMul g p)

The admissible response-value sets agree after the load correction.

theorem HCPolySupport.HighContrast.Response.responseJ_subSkew_of_ae {d : ℕ} {U : Book.Ch02.Domain d} {a b : Book.Ch02.CoeffOn U} (g : Mat d) (hg : IsSkewMat g) (hshift : b.toCoeffField =ᵐ[volumeMeasureOn U.carrier] fun (x : Vec d) => a.toCoeffField x - g) (p q : Vec d) : Book.Ch02.responseJ U b p q = Book.Ch02.responseJ U a p (q - matVecMul g p)

Constant-skew covariance of the Chapter 2 response functional.

theorem HCPolySupport.HighContrast.Response.responseJ_subSkew {d : ℕ} (U : Book.Ch02.Domain d) (a : CoeffSpace d) (g : Mat d) (hg : IsSkewMat g) (p q : Vec d) : Book.Ch02.responseJ U ((a.subSkew g hg).coeffOn U) p q = Book.Ch02.responseJ U (a.coeffOn U) p (q - matVecMul g p)

Constant-skew covariance specialized to the recentered coefficient sample.