← Mathematical handbook

theorem Papers.AnsariRockel2024.huslerReiss_pickands_antitone (δ ε : ℝ) (hδ : 0 < δ) (hε : 0 < ε) (hδε : δ ≤ ε) (t : ↑unitInterval) (ht : ↑t ∈ Set.Ioo 0 1) : Verification.copulaPickands (Verification.huslerReissPositive ε hε) t ≤ Verification.copulaPickands (Verification.huslerReissPositive δ hδ) t

theorem Papers.AnsariRockel2024.huslerReiss_lowerOrthant_mono (δ ε : ℝ) (hδ : 0 < δ) (hε : 0 < ε) (hδε : δ ≤ ε) : (Verification.huslerReissPositive δ hδ).LowerOrthantLE (Verification.huslerReissPositive ε hε)

theorem Papers.AnsariRockel2024.huslerReiss_schurBoth_mono (δ ε : ℝ) (hδ : 0 < δ) (hε : 0 < ε) (hδε : δ ≤ ε) : (Verification.huslerReissPositive δ hδ).SchurBothLE (Verification.huslerReissPositive ε hε)

theorem Papers.AnsariRockel2024.huslerReiss_lowerOrthant_iff (δ ε : ℝ) (hδ : 0 < δ) (hε : 0 < ε) : (Verification.huslerReissPositive δ hδ).LowerOrthantLE (Verification.huslerReissPositive ε hε) ↔ δ ≤ ε

theorem Papers.AnsariRockel2024.huslerReiss_schurBoth_iff (δ ε : ℝ) (hδ : 0 < δ) (hε : 0 < ε) : (Verification.huslerReissPositive δ hδ).SchurBothLE (Verification.huslerReissPositive ε hε) ↔ δ ≤ ε