High-contrast homogenization: Provider.PolynomialHomogenization.NormalizedResponseCell

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

Exact doubled-response normalization on adapted cells

The constant-skew, scalar, and exact affine covariance formulas compose with their distinct transformed primal and dual loads on every aligned cell.

theorem HCPolySupport.HighContrast.doubledResponseJ_normalizedReferenceCell {d : ℕ} [NeZero d] (a : CoeffSpace d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (t k : ℤ) (w : Fin d → ℤ) (aRef : Book.Ch03.CoeffFamily d) (haRef : ∀ (Q : TriadicCube d), (aRef.coeffOn Q).toCoeffField = affineCoefficient (Selection.normalizedRoot (symmPart abar)) ⋯ ((normalizedCenteredCoeff a abar hS).coeffOn (Response.adaptedDomain ⋯ t)).toCoeffField) (P Q : BlockVec d) : Book.Ch02.doubledResponseJ (Book.Ch02.cubeDomain (translateCube w (originCube d k))) (aRef.coeffOn (translateCube w (originCube d k))) (normalizedReferencePrimalLoad abar P) (normalizedReferenceDualLoad abar Q) = Book.Ch02.doubledResponseJ (Response.adaptedDomainAt ⋯ k w) (a.coeffOn (Response.adaptedDomainAt ⋯ k w)) P Q

The exact skew, scalar, and affine normalizations compose with all loads transformed.