← Mathematical handbook

The negative-parameter bivariate Clayton family

This branch is bivariate: negative parameters do not give the same admissible range in all dimensions. Truncation is performed before taking the power.

noncomputable def ProbabilityTheory.Copula.claytonNegative (θ : ℝ) (hθ : -1 ≤ θ) (hn : θ < 0) : Copula 2

Clayton for the full negative bivariate range −1 ≤ θ < 0.

Equations

• ProbabilityTheory.Copula.claytonNegative θ hθ hn = (ProbabilityTheory.Copula.truncatedLinearGenerator.innerPower (-θ)⁻¹ ⋯).copula

theorem ProbabilityTheory.Copula.isArchimedean_claytonNegative (θ : ℝ) (hθ : -1 ≤ θ) (hn : θ < 0) : (claytonNegative θ hθ hn).IsArchimedean

theorem ProbabilityTheory.Copula.cdf_claytonNegative (θ : ℝ) (hθ : -1 ≤ θ) (hn : θ < 0) (u : Fin 2 → ↑unitInterval) (hu : ∀ (i : Fin 2), u i ≠ 0) : (claytonNegative θ hθ hn).cdf u = max 0 (↑(u 0) ^ (-θ) + ↑(u 1) ^ (-θ) - 1) ^ (-θ)⁻¹

@[simp]

theorem ProbabilityTheory.Copula.claytonNegative_neg_one : claytonNegative (-1) ⋯ ⋯ = countermonotonic