← Mathematical handbook

The Clayton CDF

The gamma Laplace transform identifies the joint tails of the exponential/gamma ratios. Inverting the marginal CDFs then gives the usual Archimedean formula.

theorem ProbabilityTheory.Copula.claytonLaw_lowerTail {d : ℕ} (θ : ℝ) (hθ : 0 < θ) (s : Finset (Fin d)) (t : Fin d → ℝ) (ht : ∀ i ∈ s, 0 ≤ t i) : ↑(claytonLaw d θ hθ) {x : Fin d → ℝ | ∀ i ∈ s, x i ≤ -t i} = ENNReal.ofReal ((1 + ∑ i ∈ s, t i) ^ (-θ⁻¹))

Joint lower tails of any selected negative exponential/gamma ratios.

theorem ProbabilityTheory.Copula.cdf_claytonLaw_marginal {d : ℕ} (θ : ℝ) (hθ : 0 < θ) (i : Fin d) {t : ℝ} (ht : 0 ≤ t) : ↑(ProbabilityTheory.cdf (marginal (claytonLaw d θ hθ) i)) (-t) = (1 + t) ^ (-θ⁻¹)

The marginal CDF of the negative ratio at a nonpositive argument.

theorem ProbabilityTheory.Copula.claytonLaw_real_Iic {d : ℕ} (θ : ℝ) (hθ : 0 < θ) (t : Fin d → ℝ) (ht : ∀ (i : Fin d), 0 ≤ t i) : (↑(claytonLaw d θ hθ)).real (Set.Iic fun (i : Fin d) => -t i) = (1 + ∑ i : Fin d, t i) ^ (-θ⁻¹)

Joint CDF of the negative exponential/gamma ratios.

theorem ProbabilityTheory.Copula.cdf_clayton_of_pos {d : ℕ} (θ : ℝ) (hθ : 0 < θ) (u : Fin d → ↑unitInterval) (hu : ∀ (i : Fin d), 0 < ↑(u i)) : (clayton d θ hθ).cdf u = (1 + ∑ i : Fin d, (↑(u i) ^ (-θ) - 1)) ^ (-θ⁻¹)

The explicit Clayton CDF when every coordinate is positive.

theorem ProbabilityTheory.Copula.cdf_clayton {d : ℕ} (θ : ℝ) (hθ : 0 < θ) (u : Fin d → ↑unitInterval) (hu : ∀ (i : Fin d), 0 < ↑(u i)) : (clayton d θ hθ).cdf u = (∑ i : Fin d, ↑(u i) ^ (-θ) - ↑d + 1) ^ (-1 / θ)

The familiar sum-minus-dimension form of the positive-coordinate Clayton CDF.

theorem ProbabilityTheory.Copula.cdf_clayton_of_zero {d : ℕ} (θ : ℝ) (hθ : 0 < θ) (u : Fin d → ↑unitInterval) (i : Fin d) (hi : u i = 0) : (clayton d θ hθ).cdf u = 0

The Clayton CDF vanishes on every lower face of the cube.