High-contrast homogenization:

Provider.PolynomialHomogenization.Root.RowSupply.MidpointResponseOrder

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

Midpoint response order

The response order is chosen midway between half the physical block-row weight and the printed certificate order. The resulting two strict margins are equal, while the squared response row retains a positive summability gap.

noncomputable def HCPolySupport.HighContrast.RowSupply.midpointResponseOrder (g : ℝ) : ℝ

The midpoint of printRowOrder g / 2 and printCertificateOrder g.

Equations

• HCPolySupport.HighContrast.RowSupply.midpointResponseOrder g = (3 + 5 * g) / 16

theorem HCPolySupport.HighContrast.RowSupply.midpointResponseOrder_margins {g : ℝ} (hg : g ∈ Set.Ico 0 1) : 0 < midpointResponseOrder g ∧ Certificate.printRowOrder g / 2 < midpointResponseOrder g ∧ midpointResponseOrder g < Certificate.printCertificateOrder g ∧ 2 * midpointResponseOrder g - Certificate.printRowOrder g = (1 - g) / 8 ∧ 1 - 2 * midpointResponseOrder g = 5 * (1 - g) / 8 ∧ midpointResponseOrder g < 1 / 2

theorem HCPolySupport.HighContrast.RowSupply.printRowOrder_lt_twice_midpointResponseOrder {g : ℝ} (hg : g ∈ Set.Ico 0 1) : Certificate.printRowOrder g < 2 * midpointResponseOrder g