theorem
Verification.huslerReissStableTail_formula
(δ x y : ℝ)
(hδ : 0 < δ)
(hx : 0 < x)
(hy : 0 < y)
:
(huslerReissStableTail δ).value x y = x * ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) (1 / δ + δ / 2 * Real.log (x / y)) + y * ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) (1 / δ + δ / 2 * Real.log (y / x))
theorem
Verification.huslerReissPositive_pickands_formula
(δ : ℝ)
(hδ : 0 < δ)
(t : ↑unitInterval)
(ht : ↑t ∈ Set.Ioo 0 1)
:
copulaPickands (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
Verification.huslerReissPositive_cdf_interior
(δ : ℝ)
(hδ : 0 < δ)
(u v : ↑unitInterval)
(hu : ↑u ∈ Set.Ioo 0 1)
(hv : ↑v ∈ Set.Ioo 0 1)
:
(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))))