← Mathematical handbook

Squared distance between conditional CDFs

The integrated squared difference separates copulas even though conditional distributions are only defined almost everywhere. In particular, Chatterjee's xi is zero exactly at independence. No density is assumed.

theorem ProbabilityTheory.Copula.ext_conditionalCDF_ae {C D : Copula 2} (h : ∀ᵐ (v : ↑unitInterval), (fun (u : ↑unitInterval) => C.conditionalCDF u v) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => D.conditionalCDF u v) : C = D

Nested almost-everywhere equality of conditional CDFs determines the copula.

theorem ProbabilityTheory.Copula.integrable_conditionalCDF_sub_sq (C D : Copula 2) (v : ↑unitInterval) : MeasureTheory.Integrable (fun (u : ↑unitInterval) => (C.conditionalCDF u v - D.conditionalCDF u v) ^ 2) MeasureTheory.volume

theorem ProbabilityTheory.Copula.integrable_integral_conditionalCDF_sub_sq (C D : Copula 2) : MeasureTheory.Integrable (fun (v : ↑unitInterval) => ∫ (u : ↑unitInterval), (C.conditionalCDF u v - D.conditionalCDF u v) ^ 2) MeasureTheory.volume

noncomputable def ProbabilityTheory.Copula.conditionalCDFDistanceSq (C D : Copula 2) : ℝ

Squared L² distance between the two conditional CDFs on the unit square.

Equations

• C.conditionalCDFDistanceSq D = ∫ (v : ↑unitInterval) (u : ↑unitInterval), (C.conditionalCDF u v - D.conditionalCDF u v) ^ 2

theorem ProbabilityTheory.Copula.conditionalCDFDistanceSq_nonneg (C D : Copula 2) : 0 ≤ C.conditionalCDFDistanceSq D

theorem ProbabilityTheory.Copula.conditionalCDFDistanceSq_comm (C D : Copula 2) : C.conditionalCDFDistanceSq D = D.conditionalCDFDistanceSq C

@[simp]

theorem ProbabilityTheory.Copula.conditionalCDFDistanceSq_self (C : Copula 2) : C.conditionalCDFDistanceSq C = 0

theorem ProbabilityTheory.Copula.conditionalCDFDistanceSq_eq_zero_iff (C D : Copula 2) : C.conditionalCDFDistanceSq D = 0 ↔ C = D

theorem ProbabilityTheory.Copula.conditionalCDFDistanceSq_pos_iff (C D : Copula 2) : 0 < C.conditionalCDFDistanceSq D ↔ C ≠ D

theorem ProbabilityTheory.Copula.chatterjeeXi_eq_distance_independence (C : Copula 2) : C.chatterjeeXi = 6 * C.conditionalCDFDistanceSq (independence 2)

theorem ProbabilityTheory.Copula.chatterjeeXi_eq_zero_iff (C : Copula 2) : C.chatterjeeXi = 0 ↔ C = independence 2

Chatterjee's xi detects every departure from independence, including singular laws.

theorem ProbabilityTheory.Copula.chatterjeeXi_pos_iff (C : Copula 2) : 0 < C.chatterjeeXi ↔ C ≠ independence 2