← Mathematical handbook

theorem Verification.gumbel_rho_odds_kernel (p : ℝ) {t : ℝ} (ht : t ∈ Set.Ioo 0 1) : ((1 - t) ^ 2)⁻¹ * ((t / (1 - t)) ^ (p - 1) / (1 + (t / (1 - t)) ^ p + (1 + t / (1 - t)) ^ p) ^ 2) = (t * (1 - t)) ^ (p - 1) / (1 + t ^ p + (1 - t) ^ p) ^ 2

theorem Verification.gumbel_ratio_power_integral {θ : ℝ} (hθ : 0 < θ) : ∫ (s : ℝ) in Set.Ioi 0, (1 / (1 + s + (1 + s ^ θ) ^ θ⁻¹)) ^ 2 = θ⁻¹ * ∫ (w : ℝ) in Set.Ioi 0, w ^ (θ⁻¹ - 1) / (1 + w ^ θ⁻¹ + (1 + w) ^ θ⁻¹) ^ 2

theorem Verification.gumbel_spearmanRho {θ : ℝ} (hθ : 1 ≤ θ) : (ProbabilityTheory.Copula.gumbel θ hθ).spearmanRho = (12 / θ * ∫ (t : ℝ) in 0..1, (t * (1 - t)) ^ (1 / θ - 1) / (1 + t ^ (1 / θ) + (1 - t) ^ (1 / θ)) ^ 2) - 3