← Mathematical handbook

theorem Verification.nelsen11_cdf_compact (θ : ℝ) (hθ : 0 < θ) (hθ1 : θ ≤ 1 / 2) (u v : ↑unitInterval) : (nelsen11 θ ⋯ hθ1).cdf ![u, v] = max 0 (2 - (2 - ↑u ^ θ) * (2 - ↑v ^ θ)) ^ θ⁻¹

theorem Verification.nelsen11_lowerOrthant_antitone {θ η : ℝ} (hθ0 : 0 ≤ θ) (hθ1 : θ ≤ 1 / 2) (hη0 : 0 ≤ η) (hη1 : η ≤ 1 / 2) (hθη : θ ≤ η) : (nelsen11 η hη0 hη1).LowerOrthantLE (nelsen11 θ hθ0 hθ1)

theorem Verification.nelsen11_schur_monotone {θ η : ℝ} (hθ0 : 0 ≤ θ) (hθ1 : θ ≤ 1 / 2) (hη0 : 0 ≤ η) (hη1 : η ≤ 1 / 2) (hθη : θ ≤ η) : (nelsen11 θ hθ0 hθ1).SchurBothLE (nelsen11 η hη0 hη1)