Documentation

Verification.IntegralHinge

← Mathematical handbook
theorem Verification.integral_unit_linear_hinge (h : ℝ) (hh : 0 ≤ h) (t : ↑unitInterval) :
∫ (u : ↑unitInterval), max 0 (h * (↑u - ↑t)) = h * (1 - ↑t) ^ 2 / 2

Integral of a nonnegative linear hinge on the unit interval.