← Mathematical handbook

Bernstein rank formulas and tails

The xi matrix entries are evaluated in a uniform binomial finite-difference form. This also handles the boundary rows and degree one without separate conventions.

theorem Papers.Rockel2025Approximation.bernstein_basis_integral (n : ℕ) (i : Fin (n + 1)) : ∫ (u : ↑unitInterval), (bernstein n ↑i) u = 1 / (↑n + 1)

theorem Papers.Rockel2025Approximation.bernstein_lambda_entry (n j s : ℕ) : ∫ (v : ↑unitInterval), (bernstein n j) v * (bernstein n s) v = ↑(n.choose j) * ↑(n.choose s) / ((2 * ↑n + 1) * ↑((2 * n).choose (j + s)))

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

theorem Papers.Rockel2025Approximation.bernstein_conditional_cdf (C : ProbabilityTheory.Copula 2) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) (v : ↑unitInterval) : (fun (u : ↑unitInterval) => (C.bernstein m n hm hn).conditionalCDF u v) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => ∑ i : Fin m, ∑ j : Fin n, C.cdf ![bernstein.z i.succ, bernstein.z j.succ] * Verification.bernsteinDerivative m (↑i + 1) u * (bernstein n (↑j + 1)) v

theorem Papers.Rockel2025Approximation.bernstein_xi_finite_sum (C : ProbabilityTheory.Copula 2) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) : (C.bernstein m n hm hn).chatterjeeXi = 6 * ∑ 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.bernsteinDerivativeGram m ↑i ↑r * Verification.bernsteinGram n n (↑j + 1) (↑s + 1) - 2

theorem Papers.Rockel2025Approximation.bernstein_lower_tail (C : ProbabilityTheory.Copula 2) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) : (C.bernstein m n hm hn).HasLowerTailDependence 0

theorem Papers.Rockel2025Approximation.bernstein_upper_tail (C : ProbabilityTheory.Copula 2) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) : (C.bernstein m n hm hn).HasUpperTailDependence 0