theorem
Papers.AnsariRockel2024.joeExtremeValue_weight_lowerOrthant_mono
(δ : ℝ)
(hδ : 0 < δ)
(α β α' β' : ↑unitInterval)
(hα : α ≤ α')
(hβ : β ≤ β')
:
(Verification.joeExtremeValue δ hδ α β).LowerOrthantLE (Verification.joeExtremeValue δ hδ α' β')
theorem
Papers.AnsariRockel2024.joeExtremeValue_weight_schurBoth_mono
(δ : ℝ)
(hδ : 0 < δ)
(α β α' β' : ↑unitInterval)
(hα : α ≤ α')
(hβ : β ≤ β')
:
(Verification.joeExtremeValue δ hδ α β).SchurBothLE (Verification.joeExtremeValue δ hδ α' β')
theorem
Papers.AnsariRockel2024.joeExtremeValue_allParameters_lowerOrthant_mono
(δ ε : ℝ)
(hδ : 0 < δ)
(hε : 0 < ε)
(hδε : δ ≤ ε)
(α β α' β' : ↑unitInterval)
(hα : α ≤ α')
(hβ : β ≤ β')
:
(Verification.joeExtremeValue δ hδ α β).LowerOrthantLE (Verification.joeExtremeValue ε hε α' β')
theorem
Papers.AnsariRockel2024.joeExtremeValue_allParameters_schurBoth_mono
(δ ε : ℝ)
(hδ : 0 < δ)
(hε : 0 < ε)
(hδε : δ ≤ ε)
(α β α' β' : ↑unitInterval)
(hα : α ≤ α')
(hβ : β ≤ β')
:
(Verification.joeExtremeValue δ hδ α β).SchurBothLE (Verification.joeExtremeValue ε hε α' β')