High-contrast homogenization: Provider.Regularity.PrintOrderRoundedOuterResponse #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Rounded outer response at the printed order #
The order-generic response maximum theorem applies directly at
(1 + g) / 4. This interface keeps the resulting g-dependent geometric
discount instead of replacing it by the small-order constant six.
theorem
HCPolySupport.HighContrast.printOrder_outerGeometricDiscount_inv_nonneg
{g : ℝ}
(hg : g ∈ Set.Ico 0 1)
:
The inverse boundary-layer discount at the printed order is finite for
every g ∈ [0,1).