← Copula mathematical handbook

Conditional means and the copula correlation ratio

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.integral_unit_cdf (μ : MeasureTheory.Measure ↑unitInterval) [MeasureTheory.IsProbabilityMeasure μ] : ∫ (u : ↑unitInterval), μ.real (Set.Iic u) = 1 - ∫ (v : ↑unitInterval), ↑v ∂μ

The integral of a distribution function on [0,1] is one minus its mean.

noncomputable def ProbabilityTheory.Copula.RankRegion.XiBlest.Support.conditionalMean (C : Copula 2) (t : ↑unitInterval) : ℝ

Mean of the conditional distribution of the response rank.

Equations

• ProbabilityTheory.Copula.RankRegion.XiBlest.Support.conditionalMean C t = ∫ (v : ↑unitInterval), ↑v ∂C.conditionalKernel t

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.conditionalMean_eq (C : Copula 2) (t : ↑unitInterval) : conditionalMean C t = 1 - ∫ (v : ↑unitInterval), C.conditionalCDF t v

The conditional-mean identity holds for every value of the selected Markov kernel.

noncomputable def ProbabilityTheory.Copula.RankRegion.XiBlest.Support.correlationRatio (C : Copula 2) : ℝ

The copula correlation ratio is the conditional-mean variance divided by 1/12.

Equations

• ProbabilityTheory.Copula.RankRegion.XiBlest.Support.correlationRatio C = 12 * ∫ (t : ↑unitInterval), (ProbabilityTheory.Copula.RankRegion.XiBlest.Support.conditionalMean C t - 1 / 2) ^ 2

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.conditionalIID_rho_eq_ratio (C : Copula 2) : (conditionalIID C).spearmanRho = correlationRatio C

Rho of the conditional-copy copula is the original copula correlation ratio.

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.correlationRatio_nonneg (C : Copula 2) : 0 ≤ correlationRatio C