← Mathematical handbook

Blest's weighted CDF functional

Equation (3) weights the first coordinate by 1-u. Its integral exists for every copula, including singular ones. We check monotonicity, affine mixtures, the independence normalization, and the xi=0 endpoint.

noncomputable def Papers.Rockel2026XiBlest.blestNu (C : ProbabilityTheory.Copula 2) : ℝ

Equation (3), with the first coordinate carrying Blest's weight.

Equations

• Papers.Rockel2026XiBlest.blestNu C = 24 * ∫ (x : Fin 2 → ↑unitInterval), (1 - ↑(x 0)) * C.cdf x ∂(ProbabilityTheory.Copula.independence 2).toMeasure - 2

theorem Papers.Rockel2026XiBlest.blest_integrable (C : ProbabilityTheory.Copula 2) : MeasureTheory.Integrable (fun (x : Fin 2 → ↑unitInterval) => (1 - ↑(x 0)) * C.cdf x) (ProbabilityTheory.Copula.independence 2).toMeasure

theorem Papers.Rockel2026XiBlest.blest_integral_formula (C : ProbabilityTheory.Copula 2) : blestNu C = (24 * ∫ (v : ↑unitInterval) (u : ↑unitInterval), (1 - ↑u) * C.cdf ![u, v]) - 2

The product-measure definition agrees with the source's iterated integral.

theorem Papers.Rockel2026XiBlest.xi_derivative_formula (C : ProbabilityTheory.Copula 2) : C.chatterjeeXi = (6 * ∫ (v : ↑unitInterval) (u : ↑unitInterval), deriv (C.cdfSection v) ↑u ^ 2) - 2

theorem Papers.Rockel2026XiBlest.blest_mono (C D : ProbabilityTheory.Copula 2) (h : ∀ (x : Fin 2 → ↑unitInterval), C.cdf x ≤ D.cdf x) : blestNu C ≤ blestNu D

theorem Papers.Rockel2026XiBlest.blest_mix (C D : ProbabilityTheory.Copula 2) (a : ↑unitInterval) : blestNu (C.mix D a) = ↑a * blestNu C + (1 - ↑a) * blestNu D

theorem Papers.Rockel2026XiBlest.blest_independence : blestNu (ProbabilityTheory.Copula.independence 2) = 0

theorem Papers.Rockel2026XiBlest.xi_zero_slice (C : ProbabilityTheory.Copula 2) : C.chatterjeeXi = 0 ↔ C = ProbabilityTheory.Copula.independence 2 ∧ blestNu C = 0

The xi=0 endpoint of the region in Theorem 1.1.