← Mathematical handbook

Proposition 3.1: the Bernstein density and exact Kendall trace formula

theorem Papers.Rockel2025Approximation.bernstein_density_nonnegative (C : ProbabilityTheory.Copula 2) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) (x : Fin 2 → ↑unitInterval) : 0 ≤ Verification.bernsteinDensity C m n x

theorem Papers.Rockel2025Approximation.bernstein_density (C : ProbabilityTheory.Copula 2) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) : (C.bernstein m n hm hn).toMeasure = MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal (Verification.bernsteinDensity C m n x)

theorem Papers.Rockel2025Approximation.bernstein_kernel_monotone (C : ProbabilityTheory.Copula 2) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) (u : ↑unitInterval) : Monotone (Verification.bernsteinKernel C m n u)

theorem Papers.Rockel2025Approximation.bernstein_theta_integral (k : ℕ) (i r : Fin (k + 1)) : Verification.bernsteinThetaMatrix k i r = 2 * ∫ (u : ↑unitInterval), Verification.bernsteinDerivative (k + 1) (↑i + 1) u * (bernstein (k + 1) (↑r + 1)) u

theorem Papers.Rockel2025Approximation.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] * Verification.bernsteinMixedGram m ↑i ↑r * Verification.bernsteinMixedGram n ↑j ↑s - 1

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

m,n index the positive degrees m+1,n+1; Theta includes the paper's exceptional corner.