Conditional decreasingness for negative Clayton copulas #
The proof extends convexity of each positive CDF section across the truncation point where that section vanishes. Archimedean symmetry supplies the other direction.
theorem
ProbabilityTheory.Copula.isSD_clayton_negative
(θ : ℝ)
(hθ : -1 ≤ θ)
(hn : θ < 0)
:
(claytonNegative θ hθ hn).IsSD
Every admissible negative bivariate Clayton copula is stochastically decreasing in the first coordinate.
theorem
ProbabilityTheory.Copula.isCD_clayton_negative
(θ : ℝ)
(hθ : -1 ≤ θ)
(hn : θ < 0)
:
(claytonNegative θ hθ hn).IsCD
Every admissible negative bivariate Clayton copula is conditionally decreasing in both directions.