← Mathematical handbook

Identification with package ordinal sums and exact directional coefficients

theorem Verification.normalizedCDF_prefix (C : ProbabilityTheory.Copula 2) (u v : ↑unitInterval) : ∫ (t : ↑unitInterval) in Set.Iic u, normalizedCDF C t v = C.cdf ![u, v]

theorem Verification.conditionalBlocks_eq_ordinalSum (C D : ProbabilityTheory.Copula 2) (a : ↑unitInterval) (ha0 : 0 < a) (ha1 : a < 1) : conditionalBlocks C D a ha0 ha1 = C.ordinalSum D a

theorem Verification.chatterjeeXi_ordinalSum (C D : ProbabilityTheory.Copula 2) (a : ↑unitInterval) : (C.ordinalSum D a).chatterjeeXi = 1 - ↑a ^ 2 * (1 - C.chatterjeeXi) - (1 - ↑a) ^ 2 * (1 - D.chatterjeeXi)

theorem Verification.correlationRatio_ordinalSum (C D : ProbabilityTheory.Copula 2) (a : ↑unitInterval) : correlationRatio (C.ordinalSum D a) = 1 - ↑a ^ 3 * (1 - correlationRatio C) - (1 - ↑a) ^ 3 * (1 - correlationRatio D)