High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Corrector.AffineLiouvilleLocal

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

Local Sobolev transport under an invertible linear map

Centered balls are enlarged by a fixed matrix factor before the exact affine change of variables is applied. The determinant factor in the transported energy is independent of the radius.

noncomputable def HCPolySupport.HighContrast.Root.affineBallFactor {d : ℕ} (L : Mat d) : ℝ

A positive coefficient controlling the Euclidean distortion of a fixed matrix.

Equations

• HCPolySupport.HighContrast.Root.affineBallFactor L = max 1 (HCPolySupport.Book.Ch02.matrixFrobeniusNormSq L)

theorem HCPolySupport.HighContrast.Root.one_le_affineBallFactor {d : ℕ} (L : Mat d) : 1 ≤ affineBallFactor L

theorem HCPolySupport.HighContrast.Root.matVecMul_euclideanBall_subset_scaled {d : ℕ} (L : Mat d) (R : ℝ) : (fun (y : Vec d) => matVecMul L y) '' euclideanBall d R ⊆ euclideanBall d (affineBallFactor L * R)

theorem HCPolySupport.HighContrast.Root.euclideanBall_subset_affinePullback_scaled {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) (R : ℝ) : euclideanBall d R ⊆ matImage L⁻¹ (euclideanBall d (affineBallFactor L * R))

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

The local coefficient-weighted Sobolev class is preserved by an invertible affine pullback.