← Mathematical handbook

Complete Proposition 3.1 for all positive rectangular Bernstein degrees

theorem Papers.Rockel2025Approximation.bernstein_upsilon_matrix (m : ℕ) (i r : Fin (m + 1)) : ∫ (u : ↑unitInterval), Verification.bernsteinDerivative (m + 1) (↑i + 1) u * Verification.bernsteinDerivative (m + 1) (↑r + 1) u = Verification.bernsteinUpsilonMatrix m i r

All four printed Upsilon cases, including degree one and the last row/column.

theorem Papers.Rockel2025Approximation.bernstein_lambda_matrix (n : ℕ) (j s : Fin (n + 1)) : ∫ (v : ↑unitInterval), (bernstein (n + 1) (↑j + 1)) v * (bernstein (n + 1) (↑s + 1)) v = Verification.bernsteinLambdaMatrix n j s

theorem Papers.Rockel2025Approximation.bernstein_xi_trace (C : ProbabilityTheory.Copula 2) (m n : ℕ) : (C.bernstein (m + 1) (n + 1) ⋯ ⋯).chatterjeeXi = 6 * (Verification.bernsteinUpsilonMatrix m * Verification.bernsteinGridMatrix C m n * Verification.bernsteinLambdaMatrix n * (Verification.bernsteinGridMatrix C m n).transpose).trace - 2

The exact printed xi trace expression, using the piecewise Upsilon matrix.

theorem Papers.Rockel2025Approximation.bernstein_all_coefficients (C : ProbabilityTheory.Copula 2) (m n : ℕ) : have B := C.bernstein (m + 1) (n + 1) ⋯ ⋯; have D := Verification.bernsteinGridMatrix C m n; B.spearmanRho = 12 * ∑ i : Fin (m + 1), ∑ j : Fin (n + 1), 1 / ((↑m + 2) * (↑n + 2)) * D i j - 3 ∧ B.kendallTau = 1 - (Verification.bernsteinThetaMatrix m * D * Verification.bernsteinThetaMatrix n * D.transpose).trace ∧ B.chatterjeeXi = 6 * (Verification.bernsteinUpsilonMatrix m * D * Verification.bernsteinLambdaMatrix n * D.transpose).trace - 2 ∧ B.HasLowerTailDependence 0 ∧ B.HasUpperTailDependence 0

Proposition 3.1 in full. Natural m,n encode all positive degrees m+1,n+1.