Nelsen 12 lower-orthant parameter order #
The CDF is the reciprocal of one plus a two-coordinate power norm, which decreases as its exponent increases.
theorem
ProbabilityTheory.Copula.lowerOrthantLE_nelsen12
{θ η : ℝ}
(hθ : 1 ≤ θ)
(hη : 1 ≤ η)
(hθη : θ ≤ η)
:
(nelsen12 θ hθ).LowerOrthantLE (nelsen12 η hη)
Nelsen 12 increases in lower-orthant order with its parameter.