← Copula mathematical handbook

The directional copula correlation ratio

For uniform coordinates (U,V), the ratio is Var(E[V | U]) / Var(V). Since Var(V) = 1/12, it is twelve times the squared conditional-mean deviation from 1/2. This is the variance ratio itself, without a square root. It vanishes exactly when the conditional mean is constant; it need not detect independence. Regular conditional kernels also cover singular copulas.

noncomputable def ProbabilityTheory.Copula.conditionalMean (C : Copula 2) (u : ↑unitInterval) : ℝ

Conditional mean of the second uniform coordinate given the first.

Equations

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

theorem ProbabilityTheory.Copula.measurable_conditionalMean (C : Copula 2) : Measurable C.conditionalMean

theorem ProbabilityTheory.Copula.integral_conditionalKernel (C : Copula 2) (f : ↑unitInterval → ℝ) (hf : Continuous f) : ∫ (u : ↑unitInterval), ∫ (v : ↑unitInterval), f v ∂C.conditionalKernel u = ∫ (v : ↑unitInterval), f v

Averaging a continuous function against the conditional laws recovers the uniform second marginal.

theorem ProbabilityTheory.Copula.integrable_conditionalKernel_integral (C : Copula 2) (f : ↑unitInterval → ℝ) (hf : Continuous f) : MeasureTheory.Integrable (fun (u : ↑unitInterval) => ∫ (v : ↑unitInterval), f v ∂C.conditionalKernel u) MeasureTheory.volume

theorem ProbabilityTheory.Copula.conditionalMean_mem_Icc (C : Copula 2) (u : ↑unitInterval) : C.conditionalMean u ∈ Set.Icc 0 1

@[simp]

theorem ProbabilityTheory.Copula.integral_conditionalMean (C : Copula 2) : ∫ (u : ↑unitInterval), C.conditionalMean u = 1 / 2

theorem ProbabilityTheory.Copula.integrable_conditionalMean_centered_sq (C : Copula 2) : MeasureTheory.Integrable (fun (u : ↑unitInterval) => (C.conditionalMean u - 1 / 2) ^ 2) MeasureTheory.volume

noncomputable def ProbabilityTheory.Copula.copulaCorrelationRatio (C : Copula 2) : ℝ

The copula correlation ratio, predicting coordinate 1 from coordinate 0.

Equations

• C.copulaCorrelationRatio = 12 * ∫ (u : ↑unitInterval), (C.conditionalMean u - 1 / 2) ^ 2

theorem ProbabilityTheory.Copula.copulaCorrelationRatio_nonneg (C : Copula 2) : 0 ≤ C.copulaCorrelationRatio

theorem ProbabilityTheory.Copula.conditionalMean_centered_sq_le (C : Copula 2) (u : ↑unitInterval) : (C.conditionalMean u - 1 / 2) ^ 2 ≤ ∫ (v : ↑unitInterval), (↑v - 1 / 2) ^ 2 ∂C.conditionalKernel u

theorem ProbabilityTheory.Copula.integral_unit_centered_sq : ∫ (v : ↑unitInterval), (↑v - 1 / 2) ^ 2 = 1 / 12

theorem ProbabilityTheory.Copula.copulaCorrelationRatio_le_one (C : Copula 2) : C.copulaCorrelationRatio ≤ 1

theorem ProbabilityTheory.Copula.copulaCorrelationRatio_mem_Icc (C : Copula 2) : C.copulaCorrelationRatio ∈ Set.Icc 0 1

theorem ProbabilityTheory.Copula.copulaCorrelationRatio_eq_zero_iff (C : Copula 2) : C.copulaCorrelationRatio = 0 ↔ ∀ᵐ (u : ↑unitInterval), C.conditionalMean u = 1 / 2

theorem ProbabilityTheory.Copula.copulaCorrelationRatio_eq_of_kernel_ae (C : Copula 2) (κ : Kernel ↑unitInterval ↑unitInterval) (hκ : ⇑C.conditionalKernel =ᵐ[MeasureTheory.volume] ⇑κ) : C.copulaCorrelationRatio = 12 * ∫ (u : ↑unitInterval), (∫ (v : ↑unitInterval), ↑v ∂κ u - 1 / 2) ^ 2

Changing versions of the conditional kernel does not change the ratio.

@[simp]

theorem ProbabilityTheory.Copula.copulaCorrelationRatio_independence : (independence 2).copulaCorrelationRatio = 0

theorem ProbabilityTheory.Copula.copulaCorrelationRatio_eq_one_of_function (C : Copula 2) {f : ↑unitInterval → ↑unitInterval} (hf : Measurable f) (h : ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂C.toMeasure, x 1 = f (x 0)) : C.copulaCorrelationRatio = 1

A measurable deterministic response has maximal correlation ratio.

@[simp]

theorem ProbabilityTheory.Copula.copulaCorrelationRatio_comonotonic : (comonotonic 2).copulaCorrelationRatio = 1

@[simp]

theorem ProbabilityTheory.Copula.copulaCorrelationRatio_countermonotonic : countermonotonic.copulaCorrelationRatio = 1