← Mathematical handbook

theorem Verification.joe_lowerOrthant_monotone {θ η : ℝ} (hθ : 1 ≤ θ) (hη : 1 ≤ η) (hθη : θ ≤ η) : (ProbabilityTheory.Copula.joe θ hθ).LowerOrthantLE (ProbabilityTheory.Copula.joe η hη)

theorem Verification.joe_schur_monotone {θ η : ℝ} (hθ : 1 ≤ θ) (hη : 1 ≤ η) (hθη : θ ≤ η) : (ProbabilityTheory.Copula.joe θ hθ).SchurBothLE (ProbabilityTheory.Copula.joe η hη)