← Mathematical handbook

theorem Verification.nelsen17_lowerOrthant_monotone {θ η : ℝ} (hθ : θ ≠ 0) (hη : η ≠ 0) (hθη : θ ≤ η) : (nelsen17 θ hθ).LowerOrthantLE (nelsen17 η hη)

theorem Verification.nelsen17_schur_monotone {θ η : ℝ} (hθ : θ ≠ 0) (hη : η ≠ 0) (hθ1 : -1 ≤ θ) (hθη : θ ≤ η) : (nelsen17 θ hθ).SchurBothLE (nelsen17 η hη)

theorem Verification.nelsen17_schur_antitone {θ η : ℝ} (hθ : θ ≠ 0) (hη : η ≠ 0) (hη1 : η ≤ -1) (hθη : θ ≤ η) : (nelsen17 η hη).SchurBothLE (nelsen17 θ hθ)