← Copula mathematical handbook

Quadrant dependence of Frank's family (Nelsen's family 5)

• isPQD_frank, not_isNQD_frank: for θ > 0, Frank's copula is PQD and not NQD;
• isNQD_frankNegative, not_isPQD_frankNegative: for θ < 0 it is NQD and not PQD.

The inverse generator ψ(t) = -log(1 - (1 - e^{-θ}) e^{-t}) / θ is strictly log-convex, because with w = (1 - e^{-θ}) e^{-t} one has θ² (ψ ψ'' - ψ'²) = w (-log(1 - w) - w) / (1 - w)² > 0.

theorem ProbabilityTheory.Copula.FrankQuadrant.toFun_pos {θ : ℝ} (hθ : 0 < θ) (t : ℝ) : 0 ≤ t → 0 < (frankGenerator θ hθ).toFun t

Frank's inverse generator is positive on [0, ∞).

theorem ProbabilityTheory.Copula.FrankQuadrant.strictConvexOn_log {θ : ℝ} (hθ : 0 < θ) : StrictConvexOn ℝ (Set.Ici 0) fun (t : ℝ) => Real.log ((frankGenerator θ hθ).toFun t)

Frank's generator is strictly log-convex.

theorem ProbabilityTheory.Copula.isPQD_frank (θ : ℝ) (hθ : 0 < θ) : (frank θ hθ).IsPQD

Frank's copula with θ > 0 is PQD.

theorem ProbabilityTheory.Copula.not_isNQD_frank (θ : ℝ) (hθ : 0 < θ) : ¬(frank θ hθ).IsNQD

Frank's copula with θ > 0 is not NQD.

theorem ProbabilityTheory.Copula.isNQD_frankNegative (θ : ℝ) (hθ : θ < 0) : (frankNegative θ hθ).IsNQD

Frank's copula with θ < 0 is NQD.

theorem ProbabilityTheory.Copula.not_isPQD_frankNegative (θ : ℝ) (hθ : θ < 0) : ¬(frankNegative θ hθ).IsPQD

Frank's copula with θ < 0 is not PQD.