Quadrant dependence of Joe's family (Nelsen's family 6) #
For θ > 1, Joe's copula is PQD and not NQD; for θ = 1 it is independence.
The inverse generator is ψ(t) = 1 - (1 - e^{-t})^p, p = 1/θ ∈ (0, 1). With e = e^{-t} and
z = 1 - e one finds ψ ψ'' - ψ'² = p e z^{p-2} (1 - p e) (1 - z^p) - p² z^{2p-2} e², which is
positive because z^p < 1 - p e (Bernoulli's inequality).
theorem
ProbabilityTheory.Copula.JoeQuadrant.toFun_pos
{θ : ℝ}
(hθ : 1 < θ)
(t : ℝ)
:
0 ≤ t → 0 < (joeGenerator θ ⋯).toFun t
Joe's inverse generator is positive on [0, ∞).
theorem
ProbabilityTheory.Copula.JoeQuadrant.strictConvexOn_log
{θ : ℝ}
(hθ : 1 < θ)
:
StrictConvexOn ℝ (Set.Ici 0) fun (t : ℝ) => Real.log ((joeGenerator θ ⋯).toFun t)
Joe's generator is strictly log-convex for θ > 1.