theorem
Papers.AnsariRockel2024.bb5_pickands_antitone
(θ δ ε : ℝ)
(hθ : 1 ≤ θ)
(hδ : 0 < δ)
(hε : 0 < ε)
(hδε : δ ≤ ε)
(t : ↑unitInterval)
(ht : ↑t ∈ Set.Ioo 0 1)
:
Verification.copulaPickands (Verification.bb5 θ ε hθ hε) t ≤ Verification.copulaPickands (Verification.bb5 θ δ hθ hδ) t
theorem
Papers.AnsariRockel2024.bb5_lowerOrthant_mono
(θ δ ε : ℝ)
(hθ : 1 ≤ θ)
(hδ : 0 < δ)
(hε : 0 < ε)
(hδε : δ ≤ ε)
:
(Verification.bb5 θ δ hθ hδ).LowerOrthantLE (Verification.bb5 θ ε hθ hε)
theorem
Papers.AnsariRockel2024.bb5_schurBoth_mono
(θ δ ε : ℝ)
(hθ : 1 ≤ θ)
(hδ : 0 < δ)
(hε : 0 < ε)
(hδε : δ ≤ ε)
:
(Verification.bb5 θ δ hθ hδ).SchurBothLE (Verification.bb5 θ ε hθ hε)