← Mathematical handbook

noncomputable def Verification.bernsteinDerivative (m i : ℕ) (u : ↑unitInterval) : ℝ

First-coordinate Bernstein derivative; the polynomial is evaluated on the closed interval.

Equations

• Verification.bernsteinDerivative m i u = Polynomial.eval (↑u) (Polynomial.derivative (bernsteinPolynomial ℝ m i))

theorem Verification.conditionalCDF_bernstein (C : ProbabilityTheory.Copula 2) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) (v : ↑unitInterval) : (fun (u : ↑unitInterval) => (C.bernstein m n hm hn).conditionalCDF u v) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => ∑ i : Fin (m + 1), ∑ j : Fin (n + 1), C.cdf ![bernstein.z i, bernstein.z j] * bernsteinDerivative m (↑i) u * (bernstein n ↑j) v

The conditional CDF of every rectangular Bernstein copula is its finite derivative sum.