← Mathematical handbook

noncomputable def Verification.bernsteinGridMatrix (C : ProbabilityTheory.Copula 2) (m n : ℕ) : Matrix (Fin (m + 1)) (Fin (n + 1)) ℝ

Equations

• Verification.bernsteinGridMatrix C m n i j = C.cdf ![bernstein.z i.succ, bernstein.z j.succ]

noncomputable def Verification.bernsteinThetaMatrix (k : ℕ) : Matrix (Fin (k + 1)) (Fin (k + 1)) ℝ

Equations

• Verification.bernsteinThetaMatrix k = Matrix.of (Verification.bernsteinTheta k)

theorem Verification.bernstein_tau_trace (C : ProbabilityTheory.Copula 2) (m n : ℕ) : (C.bernstein (m + 1) (n + 1) ⋯ ⋯).kendallTau = 1 - (bernsteinThetaMatrix m * bernsteinGridMatrix C m n * bernsteinThetaMatrix n * (bernsteinGridMatrix C m n).transpose).trace

Proposition 3.1's exact printed trace formula, including the exceptional corner convention.