theorem
Verification.conditionalCDF_bernstein_grid
(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,
∑ j : Fin n,
C.cdf ![bernstein.z i.succ, bernstein.z j.succ] * bernsteinDerivative m (↑i + 1) u * (bernstein n (↑j + 1)) v
theorem
Verification.bernstein_xi_gram
(C : ProbabilityTheory.Copula 2)
(m n : ℕ)
(hm : 0 < m)
(hn : 0 < n)
:
(C.bernstein m n hm hn).chatterjeeXi = 6 * ∑ i : Fin m,
∑ j : Fin n,
∑ r : Fin m,
∑ s : Fin n,
C.cdf ![bernstein.z i.succ, bernstein.z j.succ] * C.cdf ![bernstein.z r.succ, bernstein.z s.succ] * bernsteinDerivativeGram m ↑i ↑r * bernsteinGram n n (↑j + 1) (↑s + 1) - 2
Fully evaluated finite Gram contraction for Chatterjee xi of a rectangular Bernstein copula.