High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Certificate.PrintOrderCertificate

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.Certificate.printCertificateOrder (g : ℝ) : ℝ

The fractional order used by the printed row conversion.

Equations

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

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

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

Equations

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

def HCPolySupport.HighContrast.Certificate.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.Certificate.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.