Documentation

Copula.Rank.ChatterjeeCross

← Mathematical handbook

The polarized conditional-CDF functional #

This symmetric cross term gives the quadratic mixture formula for xi. Its diagonal is xi itself, its value at independence is zero, and pairing with comonotonicity gives Spearman's footrule.

source
theorem ProbabilityTheory.Copula.integrable_conditionalCDF_mul (C D : Copula 2) (v : ↑unitInterval) :
MeasureTheory.Integrable (fun (u : ↑unitInterval) => C.conditionalCDF u v * D.conditionalCDF u v) MeasureTheory.volume
source
theorem ProbabilityTheory.Copula.integrable_integral_conditionalCDF_mul (C D : Copula 2) :
MeasureTheory.Integrable (fun (v : ↑unitInterval) => ∫ (u : ↑unitInterval), C.conditionalCDF u v * D.conditionalCDF u v) MeasureTheory.volume
source
noncomputable def ProbabilityTheory.Copula.chatterjeeCross (C D : Copula 2) :
ℝ

Symmetric polarization of xi, normalized so that pairing with independence is zero. Unlike xi itself, this cross functional can be negative.

Equations
Instances For
    source
    theorem ProbabilityTheory.Copula.chatterjeeCross_comm (C D : Copula 2) :
    C.chatterjeeCross D = D.chatterjeeCross C
    source
    @[simp]
    theorem ProbabilityTheory.Copula.chatterjeeCross_self (C : Copula 2) :
    C.chatterjeeCross C = C.chatterjeeXi
    source
    @[simp]
    theorem ProbabilityTheory.Copula.chatterjeeCross_independence (C : Copula 2) :
    C.chatterjeeCross (independence 2) = 0
    source
    @[simp]
    theorem ProbabilityTheory.Copula.chatterjeeCross_independence_left (C : Copula 2) :
    (independence 2).chatterjeeCross C = 0
    source
    theorem ProbabilityTheory.Copula.conditionalCDFDistanceSq_eq_cross (C D : Copula 2) :
    6 * C.conditionalCDFDistanceSq D = C.chatterjeeXi + D.chatterjeeXi - 2 * C.chatterjeeCross D
    source
    theorem ProbabilityTheory.Copula.conditionalCDF_comonotonic (v : ↑unitInterval) :
    (fun (u : ↑unitInterval) => (comonotonic 2).conditionalCDF u v) =ᵐ[MeasureTheory.volume] (Set.Iic v).indicator fun (x : ↑unitInterval) => 1
    source
    theorem ProbabilityTheory.Copula.integral_conditionalCDF_mul_comonotonic (C : Copula 2) (v : ↑unitInterval) :
    ∫ (u : ↑unitInterval), C.conditionalCDF u v * (comonotonic 2).conditionalCDF u v = C.cdf ![v, v]

    Pairing a conditional CDF with the deterministic increasing kernel recovers the diagonal.

    source
    @[simp]
    theorem ProbabilityTheory.Copula.chatterjeeCross_comonotonic (C : Copula 2) :
    C.chatterjeeCross (comonotonic 2) = C.spearmanFootrule