← Mathematical handbook

theorem Verification.gumbel_spearmanRho_real_integral {θ : ℝ} (hθ : 1 ≤ θ) : (ProbabilityTheory.Copula.gumbel θ hθ).spearmanRho = (12 * ∫ (u : ↑unitInterval) (v : ↑unitInterval), gumbelRealCDF θ ↑u ↑v) - 3

theorem Verification.gumbel_spearmanRho_log_integral {θ : ℝ} (hθ : 1 ≤ θ) : (ProbabilityTheory.Copula.gumbel θ hθ).spearmanRho = (12 * ∫ (x : ℝ) (y : ℝ) in Set.Ioi 0, Real.exp (-(x + y + (x ^ θ + y ^ θ) ^ θ⁻¹))) - 3

theorem Verification.gumbel_log_kernel_integrable (θ : ℝ) : MeasureTheory.Integrable (fun (z : ℝ × ℝ) => Real.exp (-(z.1 + z.2 + (z.1 ^ θ + z.2 ^ θ) ^ θ⁻¹))) ((MeasureTheory.volume.restrict (Set.Ioi 0)).prod (MeasureTheory.volume.restrict (Set.Ioi 0)))

theorem Verification.gumbel_log_homogeneous {θ x s : ℝ} (hθ : 0 < θ) (hx : 0 < x) (hs : 0 < s) : x + x * s + (x ^ θ + (x * s) ^ θ) ^ θ⁻¹ = x * (1 + s + (1 + s ^ θ) ^ θ⁻¹)

theorem Verification.integral_gumbel_radial {θ s : ℝ} (hθ : 0 < θ) (hs : 0 < s) : ∫ (x : ℝ) in Set.Ioi 0, max 0 x * Real.exp (-(x + x * s + (x ^ θ + (x * s) ^ θ) ^ θ⁻¹)) = (1 / (1 + s + (1 + s ^ θ) ^ θ⁻¹)) ^ 2

theorem Verification.gumbel_spearmanRho_ratio_integral {θ : ℝ} (hθ : 1 ≤ θ) : (ProbabilityTheory.Copula.gumbel θ hθ).spearmanRho = (12 * ∫ (s : ℝ) in Set.Ioi 0, (1 / (1 + s + (1 + s ^ θ) ^ θ⁻¹)) ^ 2) - 3