← Mathematical handbook

theorem Verification.gumbelPsiDeriv_weighted_sq {p t : ℝ} (ht : 0 < t) : t * gumbelPsiDeriv p t ^ 2 = p * (p * t ^ (p - 1) * (t ^ p * Real.exp (-(2 * t ^ p))))

theorem Verification.integral_gumbelPsiDeriv_weighted_sq {p : ℝ} (hp : 0 < p) : ∫ (t : ℝ) in Set.Ioi 0, t * gumbelPsiDeriv p t ^ 2 = p / 4

theorem Verification.integral_gumbelPsiDeriv_quadrant {p : ℝ} (hp : 0 < p) : ∫ (x : ℝ) (y : ℝ) in Set.Ioi 0, gumbelPsiDeriv p (x + y) ^ 2 = p / 4

theorem Verification.gumbel_kendallTau {θ : ℝ} (hθ : 1 ≤ θ) : (ProbabilityTheory.Copula.gumbel θ hθ).kendallTau = (θ - 1) / θ