High-contrast homogenization: #
Provider.PolynomialHomogenization.Root.CorrectorDecay.IdentitySuccessorLocal
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
theorem
HCPolySupport.HighContrast.exists_identityGaugeSuccessorLocalConstant
(d : ℕ)
[NeZero d]
(g : ℝ)
(geom : RoundedGenerationAnalyticGeometry d)
(hg : g ∈ Set.Ico 0 1)
:
∃ (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)) →
∀ (m : ℤ) (e : Vec d),
scalarIdentityWeakError aIdentity (printCertificateOrder g) (m - 1) ≤ 1 →
scalarIdentityWeakError aIdentity (printCertificateOrder g) m ≤ 1 →
scalarIdentityWeakError aIdentity (printCertificateOrder g) (m + 1) ≤ 1 →
Book.Ch03.h1EnergyNormOnCube (originCube d (m - 1 - 2)) aIdentity
(successorInnerRestriction aIdentity m e).toH1 ≤ C * (scalarIdentityWeakError aIdentity (printCertificateOrder g) m + scalarIdentityWeakError aIdentity (printCertificateOrder g) (m + 1)) * euclideanNorm e
Exact-identity response pricing and Caccioppoli control the successor on the centered cube three scales inside its outer cube.