High-contrast homogenization: Provider.Regularity.LiouvilleCompatibleSlope #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Compatibility of fixed-cube Liouville slopes #
Local slope selections become one global slope because the selected canonical full-gradient classes form a compatible projective family and the canonical slope map is injective on every admissible cube.
theorem
HCPolySupport.HighContrast.exists_common_jointSlope_of_compatible_localGradients
{d : ℕ}
[NeZero d]
{a : Book.Ch02.TriadicCoeffFamily d}
{n : ℤ}
(hcoercive :
∀ (hCauchy : FiniteAffineCorrectionLocalCauchy a) (e : Vec d) (q : ℕ),
n ≤ ↑q →
euclideanNorm e ≤ 2 * euclideanNorm
(localGradientClassAverage
((have this := constantGradientOnOriginCube e ↑q;
this) + (finiteAffineCorrectionJointLocalLimit a hCauchy e).gradientComponent q)))
(hCauchy : FiniteAffineCorrectionLocalCauchy a)
(g : (q : ℕ) → ↥(LocalGradientL2 d q))
(hcompat : ∀ {q r : ℕ} (hqr : q ≤ r), (localGradientRestrict hqr) (g r) = g q)
(hslope : ∀ (q : ℕ), n ≤ ↑q → ∃ (e : Vec d), g q = (jointAffineFullGradientLinearMap a hCauchy q) e)
:
Compatible fixed-cube gradient classes represented by canonical slopes are represented by one and the same slope on every admissible cube.