High-contrast homogenization:

Provider.PolynomialHomogenization.Root.CorrectorDecay.CanonicalGaugeSpine

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

noncomputable def HCPolySupport.HighContrast.canonicalIdentityRegularityConstant (d : ℕ) [NeZero d] (g : ℝ) (hg : g ∈ Set.Ico 0 1) : ℝ

Chosen constant for the print-order dual regularity estimate of the identity coefficient.

Equations

• HCPolySupport.HighContrast.canonicalIdentityRegularityConstant d g hg = Classical.choose ⋯

theorem HCPolySupport.HighContrast.canonicalIdentityRegularity (d : ℕ) [NeZero d] (g : ℝ) (hg : g ∈ Set.Ico 0 1) : PrintOrderIdentityCubeDualRegularityWithConstant d g (canonicalIdentityRegularityConstant d g hg)

noncomputable def HCPolySupport.HighContrast.canonicalIdentitySpine (d : ℕ) [NeZero d] (g : ℝ) (hg : g ∈ Set.Ico 0 1) : PrintOrderToleranceSelectedRoundedSpine d (canonicalIdentityRegularityConstant d g hg)

Chosen rounded spine for the canonical identity regularity constant.

Equations

• HCPolySupport.HighContrast.canonicalIdentitySpine d g hg = Classical.choice ⋯

noncomputable def HCPolySupport.HighContrast.canonicalIdentityGeometry (d : ℕ) [NeZero d] (g : ℝ) (hg : g ∈ Set.Ico 0 1) : RoundedGenerationAnalyticGeometry d

Rounded analytic geometry carried by the canonical identity spine.

Equations

• HCPolySupport.HighContrast.canonicalIdentityGeometry d g hg = (HCPolySupport.HighContrast.canonicalIdentitySpine d g hg).geometry

theorem HCPolySupport.HighContrast.canonicalIdentityDualRegularity (d : ℕ) [NeZero d] (g : ℝ) (hg : g ∈ Set.Ico 0 1) : PrintOrderRoundedReferenceDualRegularityAtGeneration d g (canonicalIdentityGeometry d g hg).generation

noncomputable def HCPolySupport.HighContrast.canonicalCorrectorSmallness (d : ℕ) [NeZero d] (g : ℝ) (hg : g ∈ Set.Ico 0 1) : ℝ

Successor smallness threshold obtained from the canonical identity geometry and its dual regularity.

Equations

• HCPolySupport.HighContrast.canonicalCorrectorSmallness d g hg = HCPolySupport.HighContrast.identitySuccessorSmallness d g (HCPolySupport.HighContrast.canonicalIdentityGeometry d g hg) hg ⋯

theorem HCPolySupport.HighContrast.canonicalCorrectorSmallness_mem (d : ℕ) [NeZero d] (g : ℝ) (hg : g ∈ Set.Ico 0 1) : canonicalCorrectorSmallness d g hg ∈ Set.Ioo 0 1

theorem HCPolySupport.HighContrast.exists_canonicalIdentityGaugeFamily {d : ℕ} [NeZero d] {g : ℝ} {a : CoeffSpace d} {abar : Mat d} {amplitude kappa x : ℝ} (hg : g ∈ Set.Ico 0 1) (hcert : PrintOrderQuantitativeNormalizedReferenceCertificate abar g amplitude kappa x a) : ∃ (hS : Matrix.PosDef (symmPart abar)) (hI : Matrix.PosDef (symmPart 1)) (aIdentity : Book.Ch03.CoeffFamily d), (∀ (Q : TriadicCube d), (aIdentity.coeffOn Q).toCoeffField = ↑↑((canonicalIdentityGeometry d g hg).centeredCoeffSpace 1 hI (exactGaugeCoeffSpace a abar hS))) ∧ ScalarIdentityPowerTail aIdentity (printCertificateOrder g) amplitude kappa x