Documentation
Verification
.
IntegralHinge
Search
return to top
source
Imports
Init
Copula.Rank.Integration
Imported by
Verification
.
integral_unit_linear_hinge
← Mathematical handbook
source
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.