← Mathematical handbook

noncomputable def Verification.huslerReiss (δ : ℝ) (hδ : 0 ≤ δ) : ProbabilityTheory.Copula 2

Equations

• Verification.huslerReiss δ hδ = if h : δ = 0 then ProbabilityTheory.Copula.independence 2 else Verification.huslerReissPositive δ ⋯

theorem Papers.AnsariRockel2024.huslerReiss_zero : Verification.huslerReiss 0 ⋯ = ProbabilityTheory.Copula.independence 2

theorem Papers.AnsariRockel2024.huslerReiss_positive (δ : ℝ) (hδ : 0 < δ) : Verification.huslerReiss δ ⋯ = Verification.huslerReissPositive δ hδ

theorem Papers.AnsariRockel2024.huslerReiss_closed_isExtremeValue (δ : ℝ) (hδ : 0 ≤ δ) : (Verification.huslerReiss δ hδ).IsExtremeValue

theorem Papers.AnsariRockel2024.huslerReiss_closed_isCI (δ : ℝ) (hδ : 0 ≤ δ) : (Verification.huslerReiss δ hδ).IsCI

theorem Papers.AnsariRockel2024.huslerReiss_closed_tails (δ : ℝ) (hδ : 0 ≤ δ) : (Verification.huslerReiss δ hδ).HasLowerTailDependence 0 ∧ (Verification.huslerReiss δ hδ).HasUpperTailDependence (if δ = 0 then 0 else 2 - 2 * ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) (1 / δ))

theorem Papers.AnsariRockel2024.huslerReiss_closed_lowerOrthant_mono (δ ε : ℝ) (hδ : 0 ≤ δ) (hε : 0 ≤ ε) (hδε : δ ≤ ε) : (Verification.huslerReiss δ hδ).LowerOrthantLE (Verification.huslerReiss ε hε)

theorem Papers.AnsariRockel2024.huslerReiss_closed_schurBoth_mono (δ ε : ℝ) (hδ : 0 ≤ δ) (hε : 0 ≤ ε) (hδε : δ ≤ ε) : (Verification.huslerReiss δ hδ).SchurBothLE (Verification.huslerReiss ε hε)

theorem Papers.AnsariRockel2024.huslerReiss_closed_lowerOrthant_iff (δ ε : ℝ) (hδ : 0 ≤ δ) (hε : 0 ≤ ε) : (Verification.huslerReiss δ hδ).LowerOrthantLE (Verification.huslerReiss ε hε) ↔ δ ≤ ε

theorem Papers.AnsariRockel2024.huslerReiss_closed_schurBoth_iff (δ ε : ℝ) (hδ : 0 ≤ δ) (hε : 0 ≤ ε) : (Verification.huslerReiss δ hδ).SchurBothLE (Verification.huslerReiss ε hε) ↔ δ ≤ ε