High-contrast homogenization:

Provider.PolynomialHomogenization.Root.CorrectorDecay.IdentitySuccessorRecurrence

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

theorem HCPolySupport.HighContrast.exists_identityGaugeSuccessorRecurrenceConstant (d : ℕ) [NeZero d] (g : ℝ) (geom : RoundedGenerationAnalyticGeometry d) (hg : g ∈ Set.Ico 0 1) (hdual : PrintOrderRoundedReferenceDualRegularityAtGeneration d g geom.generation) : ∃ (C : ℝ), 1 ≤ 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)) → ∀ (q m : ℤ) (e : Vec d), q ≤ m - 1 - 2 → ScalarIdentityGoodMaxOnInterval aIdentity (printCertificateOrder g) 1 q (m - 1 - 2) → ∀ h ∈ Finset.Icc q (m - 1 - 2), finiteCenteredCubeSolutionEnergy aIdentity (m - 1 - 2) (successorInnerRestriction aIdentity m e) h ≤ C * finiteCenteredCubeSolutionEnergy aIdentity (m - 1 - 2) (successorInnerRestriction aIdentity m e) (m - 1 - 2) + C * ∑ j ∈ Finset.Ioc h (m - 1 - 2), scalarIdentityWeakError aIdentity (printCertificateOrder g) j * finiteCenteredCubeSolutionEnergy aIdentity (m - 1 - 2) (successorInnerRestriction aIdentity m e) j

The available selected-generation recurrence, specialized to an exact identity-gauge family and to the successor restriction.