High-contrast homogenization: Analytic.AffineFields

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

Fields in the symmetric affine normalization

The symmetric square-root change of variables sends physical gradients and skew-centered fluxes to the two fields used by the deterministic comparison.

theorem HCPolySupport.HighContrast.matSqrt_gradient_difference_eq {d : ℕ} (S : Mat d) (F G : Vec d) : matVecMul (matSqrt S) F - matVecMul (matSqrt S) G = matVecMul (matSqrt S) (F - G)

The square-root map carries a gradient difference to the difference of the transformed gradients.

theorem HCPolySupport.HighContrast.matSqrt_inv_centered_flux_difference_eq {d : ℕ} {S A : Mat d} (hS : Matrix.PosDef S) (F G : Vec d) : matVecMul ((matSqrt S)⁻¹ * A * matTranspose (matSqrt S)⁻¹) (matVecMul (matSqrt S) F) - matVecMul (matSqrt S) G = matVecMul (matSqrt S)⁻¹ (matVecMul A F - matVecMul S G)

Inverse-square-root congruence carries the centered flux difference to the normalized flux difference.

theorem HCPolySupport.HighContrast.matSqrt_inv_skewCentered_flux_difference_eq {d : ℕ} {abar A : Mat d} (hS : Matrix.PosDef (symmPart abar)) (F G : Vec d) : matVecMul ((matSqrt (symmPart abar))⁻¹ * (A - skewPart abar) * matTranspose (matSqrt (symmPart abar))⁻¹) (matVecMul (matSqrt (symmPart abar)) F) - matVecMul (matSqrt (symmPart abar)) G = matVecMul (matSqrt (symmPart abar))⁻¹ (matVecMul (A - skewPart abar) F - matVecMul (symmPart abar) G)

The preceding identity in the skew-centered convention of the homogenization theorem.