theorem
Papers.AnsariRockel2024.frank_lowerOrthant_monotone
{θ η : ℝ}
(hθη : θ ≤ η)
:
(frankSigned θ).LowerOrthantLE (frankSigned η)
theorem
Papers.AnsariRockel2024.frank_schur_nonnegative
{θ η : ℝ}
(hθ : 0 ≤ θ)
(hθη : θ ≤ η)
:
(frankSigned θ).SchurBothLE (frankSigned η)
theorem
Papers.AnsariRockel2024.frank_schur_nonpositive
{θ η : ℝ}
(hη : η ≤ 0)
(hθη : θ ≤ η)
:
(frankSigned η).SchurBothLE (frankSigned θ)