← Copula mathematical handbook

Exact rho, footrule, gamma and beta of the FGM family

theorem ProbabilityTheory.Copula.integral_unit_mul_one_sub : ∫ (t : ↑unitInterval), ↑t * (1 - ↑t) = 1 / 6

theorem ProbabilityTheory.Copula.integral_unit_sq_mul_one_sub_sq : ∫ (t : ↑unitInterval), ↑t ^ 2 * (1 - ↑t) ^ 2 = 1 / 30

theorem ProbabilityTheory.Copula.spearmanRho_fgm (θ : ℝ) (hθ : |θ| ≤ 1) : (fgm θ hθ).spearmanRho = θ / 3

theorem ProbabilityTheory.Copula.integral_diagonal_fgm (θ : ℝ) (hθ : |θ| ≤ 1) : ∫ (t : ↑unitInterval), (fgm θ hθ).cdf ![t, t] = 1 / 3 + θ / 30

theorem ProbabilityTheory.Copula.integral_antidiagonal_fgm (θ : ℝ) (hθ : |θ| ≤ 1) : ∫ (t : ↑unitInterval), (fgm θ hθ).cdf ![t, unitInterval.symm t] = 1 / 6 + θ / 30

theorem ProbabilityTheory.Copula.spearmanFootrule_fgm (θ : ℝ) (hθ : |θ| ≤ 1) : (fgm θ hθ).spearmanFootrule = θ / 5

theorem ProbabilityTheory.Copula.giniGamma_fgm (θ : ℝ) (hθ : |θ| ≤ 1) : (fgm θ hθ).giniGamma = 4 * θ / 15

theorem ProbabilityTheory.Copula.blomqvistBeta_fgm (θ : ℝ) (hθ : |θ| ≤ 1) : (fgm θ hθ).blomqvistBeta = θ / 4