theorem
Papers.AnsariRockel2024.huslerReiss_pickands_interior
(δ : ℝ)
(hδ : 0 < δ)
(t : ↑unitInterval)
(ht : ↑t ∈ Set.Ioo 0 1)
:
Verification.copulaPickands (Verification.huslerReissPositive δ hδ) t = (1 - ↑t) * ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) (1 / δ + δ / 2 * Real.log ((1 - ↑t) / ↑t)) + ↑t * ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) (1 / δ + δ / 2 * Real.log (↑t / (1 - ↑t)))
theorem
Papers.AnsariRockel2024.huslerReiss_cdf_interior
(δ : ℝ)
(hδ : 0 < δ)
(u v : ↑unitInterval)
(hu : ↑u ∈ Set.Ioo 0 1)
(hv : ↑v ∈ Set.Ioo 0 1)
:
(Verification.huslerReissPositive δ hδ).cdf ![u, v] = Real.exp
(-(-Real.log ↑u * ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1))
(1 / δ + δ / 2 * Real.log (-Real.log ↑u / -Real.log ↑v)) + -Real.log ↑v * ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1))
(1 / δ + δ / 2 * Real.log (-Real.log ↑v / -Real.log ↑u))))