High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Corrector.LiouvilleGaugeInvariance

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

Scalar and constant-skew invariance of the Liouville class

Positive coefficient scaling changes the local symmetric energy by a fixed factor. Constant skew shifts leave that energy unchanged; their weak pairing vanishes locally on the exhaustion cubes and hence globally.

theorem HCPolySupport.HighContrast.Root.memLiouvilleClass_smul_coefficient_iff {d : ℕ} {b : CoeffField d} {theta : ℝ} {v : Vec d → ℝ} {Dv : Vec d → Vec d} {c : ℝ} (hc : 0 < c) : MemLiouvilleClass (fun (x : Vec d) => c • b x) theta v Dv ↔ MemLiouvilleClass b theta v Dv

Positive scalar multiplication of a coefficient leaves its full Liouville class unchanged.

theorem HCPolySupport.HighContrast.Root.memLiouvilleClass_add_constSkew_iff {d : ℕ} [NeZero d] {b : CoeffField d} {theta : ℝ} (hb : IsAELocallyUniformlyElliptic b) (k : Mat d) (hk : IsSkewMat k) (v : Vec d → ℝ) (Dv : Vec d → Vec d) : MemLiouvilleClass (fun (x : Vec d) => b x + k) theta v Dv ↔ MemLiouvilleClass b theta v Dv

Adding a constant skew matrix leaves the full Liouville class unchanged.