← Copula mathematical handbook

The cubic Spearman rho–Blomqvist beta bounds

The classical bounds recalled by Kokol Bukovšek et al. are proved from the package's displacement moment and median quadrant probabilities. A tent potential certifies the lower bound on squared displacement. Boundary attainment and the exact-region theorem are provided in Copula.Rank.Region.Beta.

def ProbabilityTheory.Copula.medianCrossing : Set (Fin 2 → ↑unitInterval)

Exactly one coordinate lies below the median.

Equations

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

theorem ProbabilityTheory.Copula.measurableSet_medianCrossing : MeasurableSet medianCrossing

theorem ProbabilityTheory.Copula.integral_medianCrossing (C : Copula 2) : ∫ (x : Fin 2 → ↑unitInterval), medianCrossing.indicator (fun (x : Fin 2 → ↑unitInterval) => 1) x ∂C.toMeasure = (1 - C.blomqvistBeta) / 2

theorem ProbabilityTheory.Copula.spearmanRho_le_beta (C : Copula 2) : C.spearmanRho ≤ 1 - 3 / 16 * (1 - C.blomqvistBeta) ^ 3

theorem ProbabilityTheory.Copula.beta_le_spearmanRho (C : Copula 2) : 3 / 16 * (1 + C.blomqvistBeta) ^ 3 - 1 ≤ C.spearmanRho