← Copula mathematical handbook

Spearman rho of the two-parameter Marshall–Olkin family

theorem ProbabilityTheory.Copula.integral_marshallOlkin_cdf (α β : ↑unitInterval) (hb : 0 < ↑β) : ∫ (x : Fin 2 → ↑unitInterval), (marshallOlkin α β).cdf x = (↑α + ↑β) / (2 * (2 * ↑α + 2 * ↑β - ↑α * ↑β))

theorem ProbabilityTheory.Copula.marshallOlkin_spearmanRho_pos (α β : ↑unitInterval) (hb : 0 < ↑β) : (marshallOlkin α β).spearmanRho = 3 * ↑α * ↑β / (2 * ↑α + 2 * ↑β - ↑α * ↑β)

theorem ProbabilityTheory.Copula.marshallOlkin_spearmanRho (α β : ↑unitInterval) : (marshallOlkin α β).spearmanRho = 3 * ↑α * ↑β / (2 * ↑α + 2 * ↑β - ↑α * ↑β)