← Mathematical handbook

theorem Verification.tawn_pickands (θ : ℝ) (hθ : 1 ≤ θ) (α β t : ↑unitInterval) : copulaPickands (ProbabilityTheory.Copula.tawn θ hθ α β) t = (1 - ↑α) * (1 - ↑t) + (1 - ↑β) * ↑t + ((↑α * (1 - ↑t)) ^ θ + (↑β * ↑t) ^ θ) ^ θ⁻¹

Table 4's asymmetric logistic Pickands function, identified from the actual copula.

theorem Verification.gumbel_pickands (θ : ℝ) (hθ : 1 ≤ θ) (t : ↑unitInterval) : copulaPickands (ProbabilityTheory.Copula.gumbel θ hθ) t = ((1 - ↑t) ^ θ + ↑t ^ θ) ^ θ⁻¹

theorem Verification.marshallOlkin_pickands (α β t : ↑unitInterval) : copulaPickands (ProbabilityTheory.Copula.marshallOlkin α β) t = 1 - min (↑α * (1 - ↑t)) (↑β * ↑t)

theorem Verification.cuadrasAuge_pickands (α t : ↑unitInterval) : copulaPickands (ProbabilityTheory.Copula.cuadrasAuge α) t = 1 - ↑α * min (1 - ↑t) ↑t