High-contrast homogenization: #
Provider.PolynomialHomogenization.Root.CorrectorDecay.PrintOrderJointTail
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
theorem
HCPolySupport.HighContrast.existsUnique_identityGaugeJointLocalEquation
(d : ℕ)
[NeZero d]
(g : ℝ)
(geom : RoundedGenerationAnalyticGeometry d)
(hg : g ∈ Set.Ico 0 1)
(hdual : PrintOrderRoundedReferenceDualRegularityAtGeneration d g geom.generation)
(aGauge : CoeffSpace d)
(hI : Matrix.PosDef (symmPart 1))
(aIdentity : Book.Ch03.CoeffFamily d)
(hIdentity : ∀ (Q : TriadicCube d), (aIdentity.coeffOn Q).toCoeffField = ↑↑(geom.centeredCoeffSpace 1 hI aGauge))
(delta : ℝ)
(n : ℤ)
(hdelta : delta ∈ Set.Ioc 0 (identitySuccessorSmallness d g geom hg hdual))
(hgood : ScalarIdentityGoodTail aIdentity (printCertificateOrder g) delta n)
:
∃! Phi : Vec d → NormalizedLocalH1Carrier d, IsFiniteAffineCorrectionJointLocalEquation aIdentity Phi
The exact-gauge local Cauchy witness produces the joint normalized limit and its fixed-cube weak equation at the printed order.
theorem
HCPolySupport.HighContrast.identityGaugeJointWeightedTail
(d : ℕ)
[NeZero d]
(g : ℝ)
(geom : RoundedGenerationAnalyticGeometry d)
(hg : g ∈ Set.Ico 0 1)
(hdual : PrintOrderRoundedReferenceDualRegularityAtGeneration d g geom.generation)
(aGauge : CoeffSpace d)
(hI : Matrix.PosDef (symmPart 1))
(aIdentity : Book.Ch03.CoeffFamily d)
(hIdentity : ∀ (Q : TriadicCube d), (aIdentity.coeffOn Q).toCoeffField = ↑↑(geom.centeredCoeffSpace 1 hI aGauge))
(delta : ℝ)
(n : ℤ)
(hdelta : delta ∈ Set.Ioc 0 (identitySuccessorSmallness d g geom hg hdual))
(hgood : ScalarIdentityGoodTail aIdentity (printCertificateOrder g) delta n)
(Phi : Vec d → NormalizedLocalH1Carrier d)
(hPhi : IsFiniteAffineCorrectionJointLocalEquation aIdentity Phi)
(e : Vec d)
(q m : ℕ)
(hnq : n ≤ ↑q)
(hqm : q + 3 ≤ m)
:
√(normalizedLocalSymmetricEnergy ⋯
((have this := constantGradientOnOriginCube e ↑q;
this) + (Phi e).gradientComponent q - finiteAffineInnerGradientClass aIdentity e q (m - q))) ≤ 2 * identitySuccessorEnergyConstant d g geom hg hdual * (1 + delta) * delta * euclideanNorm e
The printed-order exact-gauge successor estimate telescopes to a quantitative tail of the joint corrector, with no rounded-family join.
theorem
HCPolySupport.HighContrast.exists_identityGaugeJointLimitWithTail
(d : ℕ)
[NeZero d]
(g : ℝ)
(geom : RoundedGenerationAnalyticGeometry d)
(hg : g ∈ Set.Ico 0 1)
(hdual : PrintOrderRoundedReferenceDualRegularityAtGeneration d g geom.generation)
(aGauge : CoeffSpace d)
(hI : Matrix.PosDef (symmPart 1))
(aIdentity : Book.Ch03.CoeffFamily d)
(hIdentity : ∀ (Q : TriadicCube d), (aIdentity.coeffOn Q).toCoeffField = ↑↑(geom.centeredCoeffSpace 1 hI aGauge))
(delta : ℝ)
(n : ℤ)
(hdelta : delta ∈ Set.Ioc 0 (identitySuccessorSmallness d g geom hg hdual))
(hgood : ScalarIdentityGoodTail aIdentity (printCertificateOrder g) delta n)
:
∃ (Phi : Vec d → NormalizedLocalH1Carrier d),
IsFiniteAffineCorrectionJointLocalEquation aIdentity Phi ∧ ∀ (e : Vec d) (q m : ℕ),
n ≤ ↑q →
q + 3 ≤ m →
√(normalizedLocalSymmetricEnergy ⋯
((have this := constantGradientOnOriginCube e ↑q;
this) + (Phi e).gradientComponent q - finiteAffineInnerGradientClass aIdentity e q (m - q))) ≤ 2 * identitySuccessorEnergyConstant d g geom hg hdual * (1 + delta) * delta * euclideanNorm e
A sufficiently small exact-gauge print-order tail simultaneously supplies the joint limit, its equations, and its quantitative finite tail.