theorem
Papers.AnsariRockel2024.tEV_spectral_isExtremeValue
(ν r : ℝ)
(hν : 0 < ν)
(hr : r ∈ Set.Icc (-1) 1)
:
(Verification.tEV ν r hν hr).IsExtremeValue
theorem
Papers.AnsariRockel2024.tEV_spectral_isCI
(ν r : ℝ)
(hν : 0 < ν)
(hr : r ∈ Set.Icc (-1) 1)
:
(Verification.tEV ν r hν hr).IsCI
theorem
Papers.AnsariRockel2024.tEV_pickands_spectral
(ν r : ℝ)
(hν : 0 < ν)
(hr : r ∈ Set.Icc (-1) 1)
(t : ↑unitInterval)
:
Verification.copulaPickands (Verification.tEV ν r hν hr) t = ∫ (z : EuclideanSpace ℝ (Fin 2)), max ((1 - ↑t) * Verification.gaussianPositiveWeight ν (z.ofLp 0))
(↑t * Verification.gaussianPositiveWeight ν
(z.ofLp 1)) ∂ProbabilityTheory.multivariateGaussian 0 (Verification.bivariateCorrelation r)