← Mathematical handbook

theorem Verification.claytonPartial_regular {θ u v : ℝ} (hθ : 0 < θ) (hu : 0 < u) (hv : v ∈ Set.Ioc 0 1) : claytonPartial θ u v = (1 - (1 - v ^ (-θ)) * u ^ θ) ^ (-1 / θ - 1)

theorem Verification.claytonPartial_sq_regular {θ u v : ℝ} (hθ : 0 < θ) (hu : 0 < u) (hv : v ∈ Set.Ioc 0 1) : claytonPartial θ u v ^ 2 = (1 - (1 - v ^ (-θ)) * u ^ θ) ^ (-2 - 2 / θ)

theorem Verification.clayton_xi_regular_integral {θ : ℝ} (hθ : 0 < θ) : (ProbabilityTheory.Copula.clayton 2 θ hθ).chatterjeeXi = (6 * ∫ (v : ↑unitInterval) (u : ↑unitInterval), (1 - (1 - ↑v ^ (-θ)) * ↑u ^ θ) ^ (-2 - 2 / θ)) - 2

theorem Verification.clayton_chatterjeeXi {θ : ℝ} (hθ : 0 < θ) : (ProbabilityTheory.Copula.clayton 2 θ hθ).chatterjeeXi = (6 * ∫ (v : ↑unitInterval), eulerHypergeometric (1 / θ) (2 + 2 / θ) (1 / θ + 1) (1 - ↑v ^ (-θ))) - 2