High-contrast homogenization: Provider.Regularity.RoundedOuterSpatialResponsePowerTail

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

Quantitative power tails for rounded outer response maxima

The retained scalar identity power tail is applied at the enclosing normalized-root parent. The parent shift and rounded boundary losses are then bounded by one dimension-only affine constant times the witness eccentricity.

noncomputable def HCPolySupport.HighContrast.Transport.roundedOuterResponseAffineConstantSq (d : ℕ) : ℝ

Squared dimension-only constant for the rounded outer-response affine estimates.

Equations

• HCPolySupport.HighContrast.Transport.roundedOuterResponseAffineConstantSq d = max 1 (6 * ↑d * √↑d * (101 / 100)) * 10 * (1 + 3 * (100 / 99 * √↑d))

noncomputable def HCPolySupport.HighContrast.Transport.roundedOuterResponseAffineConstant (d : ℕ) : ℝ

A dimension-only constant absorbing the rounded boundary row and the normalized-root parent shift on the weak-error scale.

Equations

• HCPolySupport.HighContrast.Transport.roundedOuterResponseAffineConstant d = √(HCPolySupport.HighContrast.Transport.roundedOuterResponseAffineConstantSq d)

theorem HCPolySupport.HighContrast.Transport.roundedOuterResponseAffineConstant_pos (d : ℕ) : 0 < roundedOuterResponseAffineConstant d