High-contrast homogenization: Provider.PolynomialHomogenization.AffineCoeffFamily

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

Affine coefficient families

An invertible linear change of variables sends one globally measurable, locally uniformly elliptic coefficient representative to another such representative: the ball of a given radius is served by the constants of a ball of proportional radius. Using that same representative on every open triadic cube, with the constants of a ball containing the cube, produces the compatible coefficient family required by the deterministic comparison.

theorem HCPolySupport.HighContrast.exists_affineCoeffFamily {d : ℕ} (L : Mat d) (hL : IsUnit (Matrix.det L)) {b : CoeffField d} (hbmeas : MeasureTheory.AEStronglyMeasurable b MeasureTheory.volume) (hbEll : IsAELocallyUniformlyElliptic b) : ∃ (aL : Book.Ch03.CoeffFamily d), ∀ (Q : TriadicCube d), (aL.coeffOn Q).toCoeffField = affineCoefficient L hL b

A globally measurable, locally uniformly elliptic field produces a compatible Chapter 3 coefficient family after any invertible linear pullback: each cube reads the constants of a ball containing it.