← Mathematical handbook

theorem Verification.n19_exp_le {θ : ℝ} (hθ : 0 ≤ θ) {u : ↑unitInterval} (hu : 0 < ↑u) : Real.exp θ ≤ Real.exp (θ / ↑u)

theorem Verification.n19_cdf_log_pos {θ : ℝ} (hθ : 0 < θ) {u v : ↑unitInterval} (hu : 0 < ↑u) (hv : 0 < ↑v) : 0 < Real.log (Real.exp (θ / ↑u) + Real.exp (θ / ↑v) - Real.exp θ)

theorem Verification.nelsen19_lowerOrthant_monotone_pos {θ η : ℝ} (hθ : 0 < θ) (hη : 0 < η) (hθη : θ ≤ η) : (nelsen19 θ ⋯).LowerOrthantLE (nelsen19 η ⋯)

theorem Verification.nelsen19_lowerOrthant_monotone {θ η : ℝ} (hθ : 0 ≤ θ) (hη : 0 ≤ η) (hθη : θ ≤ η) : (nelsen19 θ hθ).LowerOrthantLE (nelsen19 η hη)

theorem Verification.nelsen19_schur_monotone {θ η : ℝ} (hθ : 0 ≤ θ) (hη : 0 ≤ η) (hθη : θ ≤ η) : (nelsen19 θ hθ).SchurBothLE (nelsen19 η hη)