← Mathematical handbook

The universal correlation-ratio bound eta <= 2 xi

theorem Verification.centered_sq_integrable (C : ProbabilityTheory.Copula 2) : MeasureTheory.Integrable (fun (p : ↑unitInterval × ↑unitInterval) => (C.conditionalCDF p.2 p.1 - ↑p.1) ^ 2) (MeasureTheory.volume.prod MeasureTheory.volume)

theorem Verification.centered_section (C : ProbabilityTheory.Copula 2) (t : ↑unitInterval) : MeasureTheory.Integrable (fun (u : ↑unitInterval) => C.conditionalCDF t u - ↑u) MeasureTheory.volume ∧ MeasureTheory.Integrable (fun (u : ↑unitInterval) => (C.conditionalCDF t u - ↑u) ^ 2) MeasureTheory.volume

theorem Verification.centered_mean (C : ProbabilityTheory.Copula 2) (t : ↑unitInterval) : ∫ (u : ↑unitInterval), C.conditionalCDF t u - ↑u = 1 / 2 - conditionalMean C t

theorem Verification.correlationRatio_le_twice_xi (C : ProbabilityTheory.Copula 2) : correlationRatio C ≤ 2 * C.chatterjeeXi

Cauchy--Schwarz in the response threshold, averaged over the predictor rank.

theorem Verification.centered_square_identity {f : ↑unitInterval → ℝ} (hi : MeasureTheory.Integrable f MeasureTheory.volume) (hs : MeasureTheory.Integrable (fun (u : ↑unitInterval) => f u ^ 2) MeasureTheory.volume) : ∫ (u : ↑unitInterval), (f u - ∫ (v : ↑unitInterval), f v) ^ 2 = (∫ (u : ↑unitInterval), f u ^ 2) - (∫ (u : ↑unitInterval), f u) ^ 2

theorem Verification.correlationRatio_eq_twice_xi_iff (C : ProbabilityTheory.Copula 2) : correlationRatio C = 2 * C.chatterjeeXi ↔ C.chatterjeeXi = 0

Equality in eta <= 2 xi is possible only at independence's coefficient pair (0,0).