High-contrast homogenization: Provider.PolynomialHomogenization.PrintOrderQuantitativeCertificate

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

Quantitative normalized-reference certificates at the printed order

The fractional order is a function of the already selected stochastic exponent g. This separates the printed route from an interface that selects one universal small order before g.

noncomputable def HCPolySupport.HighContrast.printCertificateOrder (g : ℝ) : ℝ

The fractional order used by the printed row conversion.

Equations

• HCPolySupport.HighContrast.printCertificateOrder g = (1 + g) / 4

noncomputable def HCPolySupport.HighContrast.printRowOrder (g : ℝ) : ℝ

The physical block-row weight used by the frozen random source.

Equations

• HCPolySupport.HighContrast.printRowOrder g = (1 + 3 * g) / 4

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

A quantitative normalized-reference certificate at the order selected after g in the printed route.

Equations

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

theorem HCPolySupport.HighContrast.printOrder_margins {g : ℝ} (hg : g ∈ Set.Ico 0 1) : 0 < printCertificateOrder g ∧ printCertificateOrder g < 1 / 2 ∧ 0 < printRowOrder g ∧ printRowOrder g ≤ 1 ∧ printRowOrder g - g = (1 - g) / 4 ∧ 2 * printCertificateOrder g - printRowOrder g = (1 - g) / 4 ∧ printRowOrder g < 2 * printCertificateOrder g ∧ 1 - 2 * printCertificateOrder g = (1 - g) / 2 ∧ 0 < 1 - 2 * printCertificateOrder g

All strict exponent margins used by the printed row conversion.

theorem HCPolySupport.HighContrast.PrintOrderQuantitativeNormalizedReferenceCertificate.rebase {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 * (y / x) ^ (-kappa)) kappa y a

Deterministic enlargement preserves a printed-order certificate.

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

Forgetting the retained rate gives the qualitative root certificate.