← Mathematical handbook

theorem Verification.bernstein_cdf_grid (C : ProbabilityTheory.Copula 2) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) (u : Fin 2 → ↑unitInterval) : (C.bernstein m n hm hn).cdf u = ∑ i : Fin m, ∑ j : Fin n, C.cdf ![bernstein.z i.succ, bernstein.z j.succ] * (bernstein m (↑i + 1)) (u 0) * (bernstein n (↑j + 1)) (u 1)

theorem Verification.bernstein_tau_finite_sum (C : ProbabilityTheory.Copula 2) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) : (C.bernstein m n hm hn).kendallTau = 4 * ∑ 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] * bernsteinMixedGram m ↑i ↑r * bernsteinMixedGram n ↑j ↑s - 1

Exact finite sum for Kendall tau, with every mixed Bernstein integral evaluated.