← Mathematical handbook

A uniform quantitative improvement of eta <= 2 xi

theorem Verification.cdf_centered_quantitative_gap (C : ProbabilityTheory.Copula 2) (t : ↑unitInterval) : 21 / 20 * (∫ (u : ↑unitInterval), C.conditionalCDF t u - ↑u) ^ 2 ≤ (∫ (u : ↑unitInterval), (C.conditionalCDF t u - ↑u) ^ 2) + 1 / 1000

The endpoint bounds of a CDF force a positive square-error contribution.

theorem Verification.correlationRatio_quantitative_bound (C : ProbabilityTheory.Copula 2) : 21 / 20 * correlationRatio C ≤ 2 * C.chatterjeeXi + 3 / 250

This estimate separates every xi=1/4 copula uniformly from eta=1/2.