← Mathematical handbook

Spearman rho of the two-parameter Marshall–Olkin family

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

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

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