High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Corrector.C1CanonicalPmProvider

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

Canonical finite-corrector slope reparameterization

The coefficient-weighted least-squares projection gives one linear slope map at a fixed inner and outer cube. Quantitative convergence of the finite correctors makes this map uniformly close to the identity, and sufficiently small good tails therefore make it bijective.

theorem HCPolySupport.HighContrast.Root.jointTargetHarmonicGradient_tail_of_jointLocalEquation {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (hCauchy : FiniteAffineCorrectionLocalCauchy a) (Phi : Vec d → NormalizedLocalH1Carrier d) (hPhi : IsFiniteAffineCorrectionJointLocalEquation a Phi) (q m : ℕ) (hqm2 : q + 2 ≤ m) (K : ℝ) (htail : ∀ (e : Vec d), √(normalizedLocalSymmetricEnergy ⋯ ((have this := constantGradientOnOriginCube e ↑q; this) + (Phi e).gradientComponent q - finiteAffineInnerGradientClass a e q (m - q))) ≤ K * euclideanNorm e) (e : Vec d) : have T := finiteTrialHarmonicGradientLinearMap a ⋯; have J := jointTargetHarmonicGradientLinearMap a hCauchy q; √(localHarmonicEnergy a q (J e - T e)) ≤ K * euclideanNorm e

The available joint local-limit family agrees with the harmonic target map used by the coefficient-weighted projection.