← Mathematical handbook

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

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

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

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

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