Documentation

Copula.Rank.Region.XiBlest.Support.ConditionalIID

← Copula 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.

source
theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.conditionalIID_classical (C : Copula 2) :
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.

source
noncomputable def ProbabilityTheory.Copula.RankRegion.XiBlest.Support.conditionalIID (C : Copula 2) :
Copula 2

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

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.conditionalIID_cdf (C : Copula 2) (u v : ↑unitInterval) :
    (conditionalIID C).cdf ![u, v] = ∫ (t : ↑unitInterval), C.conditionalCDF t u * C.conditionalCDF t v
    source
    theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.conditionalIID_footrule (C : Copula 2) :
    (conditionalIID C).spearmanFootrule = C.chatterjeeXi

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

    source
    theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.conditionalIID_rho (C : 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.