← Mathematical handbook

theorem Verification.n18Inv_power {θ η : ℝ} (hθ : 0 < θ) (hη : 0 < η) (u : ↑unitInterval) : n18Inv η u = n18Inv θ u ^ (η / θ)

theorem Verification.n18Psi_power {θ η t : ℝ} (hθ : 0 < θ) (hη : 0 < η) (ht : 0 ≤ t) : n18Psi η (t ^ (η / θ)) = n18Psi θ t

theorem Verification.nelsen18_lowerOrthant_monotone {θ η : ℝ} (hθ : 2 ≤ θ) (hθη : θ ≤ η) : (nelsen18 θ hθ).LowerOrthantLE (nelsen18 η ⋯)