High-contrast homogenization: Provider.Response.ProfileFiniteness #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Finiteness bridges for terminal response profiles #
Fail-closed extended nonnegative profile quantities are converted to real estimates only after an explicit finite upper bound has been established.
theorem
HCPolySupport.HighContrast.Response.toReal_le_of_le_ofReal
{x : ENNReal}
{C : ℝ}
(hC : 0 ≤ C)
(h : x ≤ ENNReal.ofReal C)
:
An extended nonnegative quantity below ofReal C has the exact real
upper bound when C is nonnegative.