High-contrast homogenization:

Provider.PolynomialHomogenization.Root.CorrectorDecay.JointNegOnePower

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

theorem HCPolySupport.HighContrast.exists_identityGaugeJointScaledNegOnePowerConstant (d : ℕ) [NeZero d] (g : ℝ) (geom : RoundedGenerationAnalyticGeometry d) (hg : g ∈ Set.Ico 0 1) (hdual : PrintOrderRoundedReferenceDualRegularityAtGeneration d g geom.generation) : ∃ C < ⊤, 0 < C ∧ ∀ (aGauge : CoeffSpace d) (hI : Matrix.PosDef (symmPart 1)) (aIdentity : Book.Ch03.CoeffFamily d), (∀ (Q : TriadicCube d), (aIdentity.coeffOn Q).toCoeffField = ↑↑(geom.centeredCoeffSpace 1 hI aGauge)) → ∀ (kappa x : ℝ), 0 < kappa → 0 < x → ScalarIdentityPowerTail aIdentity (printCertificateOrder g) (correctorTargetAmplitude (identitySuccessorSmallness d g geom hg hdual) kappa) kappa x → ∀ (Phi : Vec d → NormalizedLocalH1Carrier d), IsFiniteAffineCorrectionJointLocalEquation aIdentity Phi → ∀ (e : Vec d) (q : ℕ), x ≤ 3 ^ q → have rate := (3 ^ q / x) ^ (-kappa); triadicScaledNegOneNorm (↑q) (correctorGradientOnOriginCube Phi e ↑q) + triadicScaledNegOneNorm (↑q) (scalarIdentityCorrectorFluxDefectOnOriginCube aIdentity Phi e ↑q) ≤ C * ENNReal.ofReal (rate * euclideanNorm e)

The exact identity-gauge joint corrector inherits the inverse-side-length normalized negative-one power rate. The finite part is taken three generations out and restricted back before it is joined to the finite-to-limit remainder.