theorem
Verification.rafteryPower_lowerOrthant_monotone
{a b : ℝ}
(ha : 1 < a)
(hab : a ≤ b)
:
(rafteryPower a ha).LowerOrthantLE (rafteryPower b ⋯)
theorem
Verification.raftery_lowerOrthant_monotone
{δ η : ↑unitInterval}
(hδη : δ ≤ η)
:
(raftery δ).LowerOrthantLE (raftery η)
theorem
Verification.raftery_schur_monotone
{δ η : ↑unitInterval}
(hδη : δ ≤ η)
:
(raftery δ).SchurBothLE (raftery η)