High-contrast homogenization: Provider.Regularity.PrintOrderRoundedResponseScale

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

Rounded response scale at the printed fractional order

The boundary-layer discount is retained as a function of the exponent chosen after g. Enlarging by the corresponding affine multiplier absorbs the complete rounded-cell response loss without imposing a small-order bound.

noncomputable def HCPolySupport.HighContrast.printOrderRoundedResponseAffineConstantSq (d : ℕ) (g : ℝ) : ℝ

The squared rounded-response loss at the printed order.

Equations

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

noncomputable def HCPolySupport.HighContrast.printOrderRoundedResponseAffineConstant (d : ℕ) (g : ℝ) : ℝ

The rounded-response affine loss at the printed order.

Equations

• HCPolySupport.HighContrast.printOrderRoundedResponseAffineConstant d g = √(HCPolySupport.HighContrast.printOrderRoundedResponseAffineConstantSq d g)

theorem HCPolySupport.HighContrast.printOrderRoundedResponseAffineConstant_pos (d : ℕ) {g : ℝ} (hg : g ∈ Set.Ico 0 1) : 0 < printOrderRoundedResponseAffineConstant d g

The printed-order rounded-response affine loss is positive.