High-contrast homogenization: Analytic.AffineNormalization

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

Normalization by the homogenized symmetric geometry

After subtracting the constant homogenized skew part, conjugation by the inverse square root of the symmetric part sends the homogenized matrix to the identity. The associated domain is exactly the inverse-square-root image used to record its shape.

theorem HCPolySupport.HighContrast.affineCoefficient_matSqrt_symmPart_eq_one {d : ℕ} {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) (y : Vec d) : affineCoefficient (matSqrt (symmPart abar)) ⋯ (fun (x : Vec d) => symmPart abar) y = 1

The affine transform by the square root of a positive matrix normalizes the corresponding constant coefficient to the identity.

theorem HCPolySupport.HighContrast.matImage_matSqrt_matImage_inv {d : ℕ} {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) (U : Set (Vec d)) : matImage (matSqrt (symmPart abar)) (matImage (matSqrt (symmPart abar))⁻¹ U) = U

Returning from adapted coordinates recovers the original domain exactly.