← Mathematical handbook

Chatterjee's directional population coefficient

The direction is coordinate 1 given coordinate 0. Regular conditional distributions make the definition applicable to singular copulas too.

noncomputable def ProbabilityTheory.Copula.chatterjeeXi (C : Copula 2) : ℝ

Population Chatterjee xi, for the second coordinate given the first.

Equations

• C.chatterjeeXi = (6 * ∫ (t : ↑unitInterval) (u : ↑unitInterval), C.conditionalCDF u t ^ 2) - 2

theorem ProbabilityTheory.Copula.integrable_integral_conditionalCDF_sq (C : Copula 2) : MeasureTheory.Integrable (fun (t : ↑unitInterval) => ∫ (u : ↑unitInterval), C.conditionalCDF u t ^ 2) MeasureTheory.volume

theorem ProbabilityTheory.Copula.integral_conditionalCDF_centered_sq (C : Copula 2) (t : ↑unitInterval) : ∫ (u : ↑unitInterval), (C.conditionalCDF u t - ↑t) ^ 2 = (∫ (u : ↑unitInterval), C.conditionalCDF u t ^ 2) - ↑t ^ 2

theorem ProbabilityTheory.Copula.chatterjeeXi_eq_integral_centered_sq (C : Copula 2) : C.chatterjeeXi = 6 * ∫ (t : ↑unitInterval) (u : ↑unitInterval), (C.conditionalCDF u t - ↑t) ^ 2

The integrated conditional variance form of xi.

theorem ProbabilityTheory.Copula.chatterjeeXi_nonneg (C : Copula 2) : 0 ≤ C.chatterjeeXi

theorem ProbabilityTheory.Copula.chatterjeeXi_le_one (C : Copula 2) : C.chatterjeeXi ≤ 1

theorem ProbabilityTheory.Copula.chatterjeeXi_mem_Icc (C : Copula 2) : C.chatterjeeXi ∈ Set.Icc 0 1

theorem ProbabilityTheory.Copula.chatterjeeXi_eq_of_kernel_ae (C : Copula 2) (κ : Kernel ↑unitInterval ↑unitInterval) (hκ : ⇑C.conditionalKernel =ᵐ[MeasureTheory.volume] ⇑κ) : C.chatterjeeXi = (6 * ∫ (t : ↑unitInterval) (u : ↑unitInterval), (κ u).real (Set.Iic t) ^ 2) - 2

Any almost-everywhere equal version of the conditional kernel computes the same xi.