High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Corrector.AffineLiouvilleClass

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

Liouville-class covariance under invertible affine maps

The coefficient ellipticity calculation is the representative-level form of the packaged affine-pullback coefficient construction. It supplies the reverse local-Sobolev transport without adding a second ellipticity premise.

theorem HCPolySupport.HighContrast.Root.isEllipticMatrix_affineCoefficient {d : ℕ} (L : Mat d) (hL : IsUnit (Matrix.det L)) {b : CoeffField d} {lam Lam : ℝ} {y : Vec d} (hb : IsEllipticMatrix lam Lam (b (matVecMul L y))) : IsEllipticMatrix (lam / max 1 (Book.Ch02.matrixFrobeniusNormSq (matTranspose L))) (max Lam (Book.Ch02.matrixFrobeniusNormSq L⁻¹ * Lam)) (affineCoefficient L hL b y)

Pointwise ellipticity is preserved by an invertible divergence-form pullback, with fixed transformed constants.

theorem HCPolySupport.HighContrast.Root.isAELocallyUniformlyElliptic_affineCoefficient {d : ℕ} (L : Mat d) (hL : IsUnit (Matrix.det L)) {b : CoeffField d} (hb : IsAELocallyUniformlyElliptic b) : IsAELocallyUniformlyElliptic (affineCoefficient L hL b)

Local uniform ellipticity transports through the affine coefficient field: the ball of radius R is served by the transformed constants of a ball whose radius absorbs the matrix.

theorem HCPolySupport.HighContrast.Root.memLiouvilleClass_affinePullback_iff {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) {b : CoeffField d} {theta : ℝ} (hb : IsAELocallyUniformlyElliptic b) (v : Vec d → ℝ) (Dv : Vec d → Vec d) : MemLiouvilleClass b theta v Dv ↔ MemLiouvilleClass (affineCoefficient L hL b) theta (fun (y : Vec d) => v (matVecMul L y)) fun (y : Vec d) => matVecMul (matTranspose L) (Dv (matVecMul L y))

Full Liouville membership is equivalent before and after an invertible affine pullback.