High-contrast homogenization:

Provider.PolynomialHomogenization.Root.CorrectorDecay.IdentityGaugeSpecialization

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

Exact identity specialization of the printed rounded recurrence

In the normalized gauge, the symmetric reference is literally the identity. At an admissible rounded generation, rounding fixes that identity exactly. The lemmas below isolate this specialization and its a.e.-invariance.

theorem HCPolySupport.HighContrast.roundedReferenceMatrixAtGeneration_one {d : ℕ} [NeZero d] {l : ℤ} (hl : ↑(kZero d) ≤ l) (hI : Matrix.PosDef (symmPart 1)) : roundedReferenceMatrixAtGeneration l 1 hI = 1

theorem HCPolySupport.HighContrast.roundedCenteredCoefficientAtGeneration_one {d : ℕ} [NeZero d] {l : ℤ} (hl : ↑(kZero d) ≤ l) (hI : Matrix.PosDef (symmPart 1)) (a : CoeffField d) : roundedCenteredCoefficientAtGeneration l hl 1 hI a = a

The selected-generation centered coefficient at identity is pointwise the input coefficient. This is where the rounded construction becomes exact, rather than merely close.

theorem HCPolySupport.HighContrast.identityCenteredCoeffSpace_ae {d : ℕ} [NeZero d] (geom : RoundedGenerationAnalyticGeometry d) (hI : Matrix.PosDef (symmPart 1)) (a : CoeffSpace d) : ↑↑(geom.centeredCoeffSpace 1 hI a) =ᵐ[MeasureTheory.volume] ↑↑a

Re-rounding a gauge coefficient at the identity changes only its chosen representative, not its a.e. class.

theorem HCPolySupport.HighContrast.scalarIdentityWeakError_eq_of_aeeq {d : ℕ} {a b : Book.Ch02.TriadicCoeffFamily d} (hab : a.AEEq b) (s : ℝ) (m : ℤ) : scalarIdentityWeakError a s m = scalarIdentityWeakError b s m

A.e.-equivalent coefficient families have the same scalar-identity weak error at every scale and order.

theorem HCPolySupport.HighContrast.scalarIdentityPowerTail_of_aeeq {d : ℕ} {a b : Book.Ch02.TriadicCoeffFamily d} {s amplitude kappa x : ℝ} (hab : a.AEEq b) (h : ScalarIdentityPowerTail a s amplitude kappa x) : ScalarIdentityPowerTail b s amplitude kappa x

theorem HCPolySupport.HighContrast.roundedGenerationSpatialWeakError_one_eq {d : ℕ} [NeZero d] (geom : RoundedGenerationAnalyticGeometry d) (a : CoeffSpace d) (hI : Matrix.PosDef (symmPart 1)) (aIdentity : Book.Ch03.CoeffFamily d) (hIdentity : ∀ (Q : TriadicCube d), (aIdentity.coeffOn Q).toCoeffField = ↑↑(geom.centeredCoeffSpace 1 hI a)) (s : ℝ) (m : ℤ) : geom.spatialWeakError a 1 hI s m = scalarIdentityWeakError aIdentity s m

At identity, the selected-generation physical response row is exactly the scalar-identity homogenization error of any family realizing the selected coefficient space.

noncomputable def HCPolySupport.HighContrast.exactGaugeCoeffSpace {d : ℕ} [NeZero d] (a : CoeffSpace d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) : CoeffSpace d

The exact gauge coefficient carried by a printed certificate.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.exactGaugeCoeffSpace_ae {d : ℕ} [NeZero d] (a : CoeffSpace d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) : ↑↑(exactGaugeCoeffSpace a abar hS) =ᵐ[MeasureTheory.volume] affineCoefficient (Selection.normalizedRoot (symmPart abar)) ⋯ ↑↑(normalizedCenteredCoeff a abar hS)

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

Package the certificate's exact family on the selected identity geometry. The resulting family is a.e.-equivalent to the certificate family and retains its complete quantitative power tail.