High-contrast homogenization: Provider.PolynomialHomogenization.NormalizedLoadCovariance

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

Covariance of normalized response loads

The primal and dual loads transform differently under constant-skew removal, positive scalar normalization, and affine pullback. These load maps preserve the doubled pairing and the first two coefficient changes preserve the doubled response.

def HCPolySupport.HighContrast.skewCenteredPrimalLoad {d : ℕ} (g : Mat d) (P : BlockVec d) : BlockVec d

Primal load after subtracting a constant skew matrix.

Equations

• HCPolySupport.HighContrast.skewCenteredPrimalLoad g P = (P.1, P.2 - HCPolySupport.matVecMul g P.1)

def HCPolySupport.HighContrast.skewCenteredDualLoad {d : ℕ} (g : Mat d) (Q : BlockVec d) : BlockVec d

Dual load after subtracting a constant skew matrix.

Equations

• HCPolySupport.HighContrast.skewCenteredDualLoad g Q = (Q.1 - HCPolySupport.matVecMul g Q.2, Q.2)

noncomputable def HCPolySupport.HighContrast.scalarNormalizedPrimalLoad {d : ℕ} (alpha : ℝ) (P : BlockVec d) : BlockVec d

Primal load after multiplying the coefficient by a positive scalar.

Equations

• HCPolySupport.HighContrast.scalarNormalizedPrimalLoad alpha P = (alpha⁻¹ • P.1, alpha • P.2)

noncomputable def HCPolySupport.HighContrast.scalarNormalizedDualLoad {d : ℕ} (alpha : ℝ) (Q : BlockVec d) : BlockVec d

Dual load after multiplying the coefficient by a positive scalar.

Equations

• HCPolySupport.HighContrast.scalarNormalizedDualLoad alpha Q = (alpha • Q.1, alpha⁻¹ • Q.2)

noncomputable def HCPolySupport.HighContrast.affineReferencePrimalLoad {d : ℕ} (q : Mat d) (P : BlockVec d) : BlockVec d

Primal load under the affine pullback x = q y.

Equations

• HCPolySupport.HighContrast.affineReferencePrimalLoad q P = (HCPolySupport.matVecMul (HCPolySupport.matTranspose q) P.1, HCPolySupport.matVecMul q⁻¹ P.2)

noncomputable def HCPolySupport.HighContrast.affineReferenceDualLoad {d : ℕ} (q : Mat d) (Q : BlockVec d) : BlockVec d

Dual load under the affine pullback x = q y.

Equations

• HCPolySupport.HighContrast.affineReferenceDualLoad q Q = (HCPolySupport.matVecMul q⁻¹ Q.1, HCPolySupport.matVecMul (HCPolySupport.matTranspose q) Q.2)

noncomputable def HCPolySupport.HighContrast.normalizedReferencePrimalLoad {d : ℕ} (abar : Mat d) (P : BlockVec d) : BlockVec d

The physical-to-reference primal load for exact normalization at abar.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.HighContrast.normalizedReferenceDualLoad {d : ℕ} (abar : Mat d) (Q : BlockVec d) : BlockVec d

The physical-to-reference dual load for exact normalization at abar.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.doubledResponseJ_subSkew {d : ℕ} {U : Book.Ch02.Domain d} (a : CoeffSpace d) (g : Mat d) (hg : IsSkewMat g) (P Q : BlockVec d) : Book.Ch02.doubledResponseJ U ((a.subSkew g hg).coeffOn U) (skewCenteredPrimalLoad g P) (skewCenteredDualLoad g Q) = Book.Ch02.doubledResponseJ U (a.coeffOn U) P Q

Removing a constant skew matrix preserves the doubled response when the primal and dual loads are recentered separately.

theorem HCPolySupport.HighContrast.doubledResponseJ_positiveScale {d : ℕ} (c : ℝ) (hc : 0 < c) (a : CoeffSpace d) (U : Book.Ch02.Domain d) (P Q : BlockVec d) : Book.Ch02.doubledResponseJ U ((CoeffSpace.positiveScale c hc a).coeffOn U) (scalarNormalizedPrimalLoad (√c) P) (scalarNormalizedDualLoad (√c) Q) = Book.Ch02.doubledResponseJ U (a.coeffOn U) P Q

Positive scalar normalization preserves the doubled response when the primal and dual loads carry reciprocal square-root factors.

theorem HCPolySupport.HighContrast.blockVecDot_normalizedReferenceLoads {d : ℕ} [NeZero d] {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) (P Q : BlockVec d) : blockVecDot (normalizedReferencePrimalLoad abar P) (normalizedReferenceDualLoad abar Q) = blockVecDot P Q

The distinct normalized primal and dual load maps preserve their doubled pairing.