← Mathematical handbook

Conditional means and the copula correlation ratio

theorem Verification.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 Verification.conditionalMean (C : ProbabilityTheory.Copula 2) (t : ↑unitInterval) : ℝ

Mean of the conditional distribution of the response rank.

Equations

• Verification.conditionalMean C t = ∫ (v : ↑unitInterval), ↑v ∂C.conditionalKernel t

theorem Verification.conditionalMean_eq (C : ProbabilityTheory.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 Verification.correlationRatio (C : ProbabilityTheory.Copula 2) : ℝ

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

Equations

• Verification.correlationRatio C = 12 * ∫ (t : ↑unitInterval), (Verification.conditionalMean C t - 1 / 2) ^ 2

theorem Verification.conditionalIID_rho_eq_ratio (C : ProbabilityTheory.Copula 2) : (conditionalIID C).spearmanRho = correlationRatio C

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

theorem Verification.correlationRatio_nonneg (C : ProbabilityTheory.Copula 2) : 0 ≤ correlationRatio C