← Mathematical handbook

The copula of two conditionally independent response copies

Its distribution function is the integral of the product of the two conditional CDFs. The construction applies to every copula, including singular laws.

theorem Verification.conditionalIID_classical (C : ProbabilityTheory.Copula 2) : ProbabilityTheory.Copula.IsClassical fun (x : Fin 2 → ↑unitInterval) => ∫ (t : ↑unitInterval), C.conditionalCDF t (x 0) * C.conditionalCDF t (x 1)

Positivity of rectangle increments follows from monotonicity of each conditional CDF.

noncomputable def Verification.conditionalIID (C : ProbabilityTheory.Copula 2) : ProbabilityTheory.Copula 2

The law of two conditionally independent copies of coordinate 1 given coordinate 0.

Equations

• Verification.conditionalIID C = ProbabilityTheory.Copula.ofClassical (fun (x : Fin 2 → ↑unitInterval) => ∫ (t : ↑unitInterval), C.conditionalCDF t (x 0) * C.conditionalCDF t (x 1)) ⋯

theorem Verification.conditionalIID_cdf (C : ProbabilityTheory.Copula 2) (u v : ↑unitInterval) : (conditionalIID C).cdf ![u, v] = ∫ (t : ↑unitInterval), C.conditionalCDF t u * C.conditionalCDF t v

theorem Verification.conditionalIID_footrule (C : ProbabilityTheory.Copula 2) : (conditionalIID C).spearmanFootrule = C.chatterjeeXi

The Markov-square footrule is exactly the original directed Chatterjee coefficient.

theorem Verification.conditionalIID_rho (C : ProbabilityTheory.Copula 2) : (conditionalIID C).spearmanRho = (12 * ∫ (t : ↑unitInterval), (∫ (u : ↑unitInterval), C.conditionalCDF t u) ^ 2) - 3

Integral formula for rho of the conditional-copy law.