High-contrast homogenization: Provider.Regularity.PrintOrderEffectiveScale #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Effective-scale operations for printed-order certificates #
The deterministic scale operations do not inspect a small-order upper bound.
They therefore preserve the certificate whose order is selected after g.
theorem
HCPolySupport.HighContrast.PrintOrderQuantitativeNormalizedReferenceCertificate.targetedEffectiveScale
{d : ℕ}
[NeZero d]
{abar : Mat d}
{g amplitude target kappa : ℝ}
{X : CoeffSpace d → ℝ}
{a : CoeffSpace d}
(h : PrintOrderQuantitativeNormalizedReferenceCertificate abar g amplitude kappa (X a) a)
(hTarget : 0 < target)
:
PrintOrderQuantitativeNormalizedReferenceCertificate abar g target kappa
(targetedQuantitativeEffectiveScale amplitude target kappa X a) a
Reducing the retained amplitude to a positive target preserves the printed response order and decay exponent.
theorem
HCPolySupport.HighContrast.PrintOrderQuantitativeNormalizedReferenceCertificate.enlargeScale
{d : ℕ}
[NeZero d]
{abar : Mat d}
{a : CoeffSpace d}
{g x y amplitude kappa : ℝ}
(h : PrintOrderQuantitativeNormalizedReferenceCertificate abar g amplitude kappa x a)
(hy : 0 < y)
(hxy : x ≤ y)
:
PrintOrderQuantitativeNormalizedReferenceCertificate abar g amplitude kappa y a
Enlargement to a later positive scale preserves the same per-g
certificate and amplitude.
theorem
HCPolySupport.HighContrast.PrintOrderQuantitativeNormalizedReferenceCertificate.commonAffineScale
{d : ℕ}
[NeZero d]
{abar : Mat d}
{a : CoeffSpace d}
{g amplitude target kappaRate Caff overlinePi kappaCube : ℝ}
{X : CoeffSpace d → ℝ}
(h : PrintOrderQuantitativeNormalizedReferenceCertificate abar g amplitude kappaRate (X a) a)
(hTarget : 0 < target)
:
PrintOrderQuantitativeNormalizedReferenceCertificate abar g target kappaRate
(commonQuantitativeAffineScale amplitude target kappaRate Caff overlinePi kappaCube X a) a
The common affine enlargement preserves a printed-order certificate.