← Mathematical handbook

noncomputable def Verification.bernsteinLambdaMatrix (n : ℕ) : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ

The printed Lambda matrix for degree n+1 and source indices j+1,s+1.

Equations

• Verification.bernsteinLambdaMatrix n = Matrix.of fun (j s : Fin (n + 1)) => Verification.bernsteinGram (n + 1) (n + 1) (↑j + 1) (↑s + 1)

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

theorem Verification.bernsteinUpsilonMatrix_eq_gram (m : ℕ) (i r : Fin (m + 1)) : bernsteinUpsilonMatrix m i r = bernsteinDerivativeGram (m + 1) ↑i ↑r

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

Proposition 3.1's exact xi trace formula, with the printed piecewise Upsilon matrix.