← Mathematical handbook

theorem Verification.n13_power_comparison (r : ℝ) (hr : 1 ≤ r) {a b : ℝ} (ha : 1 ≤ a) (hb : 1 ≤ b) : a ^ r + b ^ r - 1 ≤ (a + b - 1) ^ r

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

theorem Verification.nelsen13_zero_lowerOrthant (θ : ℝ) (hθ : 0 < θ) : (nelsen13 0 ⋯).LowerOrthantLE (nelsen13 θ ⋯)

theorem Verification.nelsen13_lowerOrthant_monotone {θ η : ℝ} (hθ : 0 ≤ θ) (hη : 0 ≤ η) (hθη : θ ≤ η) : (nelsen13 θ hθ).LowerOrthantLE (nelsen13 η hη)