High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Corrector.PhysicalLiouvilleGauge

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

Physical-to-normalized Liouville transport

The physical coefficient is first recentered by its constant skew part, then positively scaled, and finally pulled back by the normalized square root.

theorem HCPolySupport.HighContrast.Root.memLiouvilleClass_physical_normalizedPullback_iff {d : ℕ} [NeZero d] (a : CoeffSpace d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) {b : CoeffField d} {theta : ℝ} (hb : IsAELocallyUniformlyElliptic b) (hcoeff : affineCoefficient (Selection.normalizedRoot (symmPart abar)) ⋯ ↑↑(normalizedCenteredCoeff a abar hS) =ᵐ[MeasureTheory.volume] b) (v : Vec d → ℝ) (Dv : Vec d → Vec d) : MemLiouvilleClass (fun (x : Vec d) => ↑↑a x) theta v Dv ↔ MemLiouvilleClass b theta (fun (y : Vec d) => v (matVecMul (Selection.normalizedRoot (symmPart abar)) y)) fun (y : Vec d) => matVecMul (matTranspose (Selection.normalizedRoot (symmPart abar))) (Dv (matVecMul (Selection.normalizedRoot (symmPart abar)) y))

Full Liouville membership is equivalent between the physical coefficient and any locally uniformly elliptic representative of its normalized affine gauge.