High-contrast homogenization:

Provider.PolynomialHomogenization.QuantitativeNormalizedReferenceCertificate

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

A rate-bearing normalized reference certificate

The deterministic regularity modules use one normalized coefficient family at one real effective scale. The certificate below retains the response order, pointwise decay exponent, amplitude, and coefficient identification instead of erasing them into a qualitative summable tail.

def HCPolySupport.HighContrast.QuantitativeNormalizedReferenceCertificate {d : ℕ} [NeZero d] (abar : Mat d) (s amplitude kappa x : ℝ) (a : CoeffSpace d) : Prop

A normalized reference family with a fixed small response order and a fixed pointwise power tail above one common real effective scale. The order, amplitude, and exponent are parameters so they are selected before a sample.

Equations

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

theorem HCPolySupport.HighContrast.QuantitativeNormalizedReferenceCertificate.rebase {d : ℕ} [NeZero d] {abar : Mat d} {a : CoeffSpace d} {x y s amplitude kappa : ℝ} (h : QuantitativeNormalizedReferenceCertificate abar s amplitude kappa x a) (hy : 0 < y) (hxy : x ≤ y) : QuantitativeNormalizedReferenceCertificate abar s (amplitude * (y / x) ^ (-kappa)) kappa y a

Deterministic enlargement preserves a quantitative normalized reference certificate, with the exact rebased amplitude and no change of family.

theorem HCPolySupport.HighContrast.QuantitativeNormalizedReferenceCertificate.to_normalizedReferenceGoodScale {d : ℕ} [NeZero d] {abar : Mat d} {a : CoeffSpace d} {x s amplitude kappa : ℝ} (h : QuantitativeNormalizedReferenceCertificate abar s amplitude kappa x a) : NormalizedReferenceGoodScale abar a x

Forgetting the retained pointwise rate gives the underlying qualitative normalized-reference certificate at the same effective scale.