Documentation
Verification
.
BernsteinIntegral
Search
return to top
source
Imports
Init
Copula.Bernstein.Basis
Copula.Rank.Integration
Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Imported by
Verification
.
integral_bernstein
← Mathematical handbook
The exact integral of every Bernstein basis function
#
source
theorem
Verification
.
integral_bernstein
(
n
:
ℕ
)
(
i
:
Fin
(
n
+
1
)
)
:
∫
(
u
:
↑
unitInterval
)
,
(
bernstein
n
↑
i
)
u
=
1
/
(
↑
n
+
1
)
Each degree-n Bernstein basis polynomial has integral 1/(n+1).