← Copula mathematical handbook

Corollary 1.7 and Remark 1.8: the exact mean-variance region

noncomputable def ProbabilityTheory.Copula.RankRegion.MeanVariance.meanDistance (C : Copula 2) : ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.MeanVariance.meanDistance C = ∫ (x : Fin 2 → ↑unitInterval), |↑(x 0) - ↑(x 1)| ∂C.toMeasure

noncomputable def ProbabilityTheory.Copula.RankRegion.MeanVariance.distanceVariance (C : Copula 2) : ℝ

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ProbabilityTheory.Copula.RankRegion.MeanVariance.maximumVariance (m : ℝ) : ℝ

Equation (23); the nonnegative real power is written as a cube of a square root.

Equations

• ProbabilityTheory.Copula.RankRegion.MeanVariance.maximumVariance m = (1 - √(1 - 2 * m) ^ 3) / 3 - m ^ 2

theorem ProbabilityTheory.Copula.RankRegion.MeanVariance.meanDistance_mem (C : Copula 2) : meanDistance C ∈ Set.Icc 0 (1 / 2)

The absolute displacement mean has precisely the admissible range [0,1/2].

theorem ProbabilityTheory.Copula.RankRegion.MeanVariance.distanceVariance_eq (C : Copula 2) : distanceVariance C = (1 - C.spearmanRho) / 6 - meanDistance C ^ 2

The affine conversion between rho and the variance at a fixed mean.

theorem ProbabilityTheory.Copula.RankRegion.MeanVariance.sharp_variance_bounds (C : Copula 2) : minimumVariance (meanDistance C) ≤ distanceVariance C ∧ distanceVariance C ≤ maximumVariance (meanDistance C)

Corollary 1.7: both sharp variance bounds.

theorem ProbabilityTheory.Copula.RankRegion.MeanVariance.minimumVariance_le_maximumVariance {m : ℝ} (hm : m ∈ Set.Icc 0 (1 / 2)) : minimumVariance m ≤ maximumVariance m

The two boundary variances are ordered throughout the admissible mean range.

theorem ProbabilityTheory.Copula.RankRegion.MeanVariance.exact_mean_variance_region (m v : ℝ) : (∃ (C : Copula 2), meanDistance C = m ∧ distanceVariance C = v) ↔ m ∈ Set.Icc 0 (1 / 2) ∧ minimumVariance m ≤ v ∧ v ≤ maximumVariance m

Remark 1.8(a): every intermediate variance is attained, and no others are.

theorem ProbabilityTheory.Copula.RankRegion.MeanVariance.maximum_variance_attained {m : ℝ} (hm : m ∈ Set.Icc 0 (1 / 2)) : ∃ (C : Copula 2), meanDistance C = m ∧ distanceVariance C = maximumVariance m

Corollary 1.7: the upper variance bound is attained for every prescribed mean.