← Mathematical handbook

The t-EV family (Tables 1, 4 and 5)

Verification.tEV ν r is the spectral extreme-value copula built from normalized positive powers of a correlated Gaussian pair. Here it is identified with the printed Student-t Pickands function, and its CI, tail, order and endpoint entries are checked. Verification.studentTCDF (ν+1) is the Student-t CDF T_{ν+1}; it coincides with the marginal CDF of the Student-t law with ν+1 degrees of freedom used for the Student-t rows.

theorem Papers.AnsariRockel2024.tEV_student_cdf_eq (ν : ℝ) (hν : 0 < ν) (x : ℝ) : Verification.studentTCDF (ν + 1) x = ↑(ProbabilityTheory.cdf (ProbabilityTheory.Copula.marginal (ProbabilityTheory.Copula.studentTLaw (Verification.bivariateCorrelation 0) (ν + 1) ⋯) 0)) x

T_{ν+1} is the marginal CDF of the standard Student-t law with ν+1 degrees of freedom.

theorem Papers.AnsariRockel2024.tEV_arg_def (ν r w : ℝ) : Verification.tEVArg ν r w = √((1 + ν) / (1 - r ^ 2)) * (w - r)

The Pickands argument z_t in the printed form sqrt((1+ν)/(1-ρ²))((t/(1-t))^(1/ν)-ρ).

theorem Papers.AnsariRockel2024.tEV_pickands (ν r : ℝ) (hν : 0 < ν) (hr : r ∈ Set.Ioo (-1) 1) (t : ↑unitInterval) (ht : ↑t ∈ Set.Ioo 0 1) : Verification.copulaPickands (Verification.tEV ν r hν ⋯) t = (1 - ↑t) * Verification.studentTCDF (ν + 1) (Verification.tEVArg ν r (((1 - ↑t) / ↑t) ^ (1 / ν))) + ↑t * Verification.studentTCDF (ν + 1) (Verification.tEVArg ν r ((↑t / (1 - ↑t)) ^ (1 / ν)))

Tables 1 and 4: the t-EV Pickands function A(t)=(1-t)T_{ν+1}(z_{1-t})+t T_{ν+1}(z_t).

theorem Papers.AnsariRockel2024.tEV_cdf_interior (ν r : ℝ) (hν : 0 < ν) (hr : r ∈ Set.Ioo (-1) 1) (u v : ↑unitInterval) (hu : ↑u ∈ Set.Ioo 0 1) (hv : ↑v ∈ Set.Ioo 0 1) : (Verification.tEV ν r hν ⋯).cdf ![u, v] = Real.exp (-(-Real.log ↑u * Verification.studentTCDF (ν + 1) (Verification.tEVArg ν r ((-Real.log ↑u / -Real.log ↑v) ^ (1 / ν))) + -Real.log ↑v * Verification.studentTCDF (ν + 1) (Verification.tEVArg ν r ((-Real.log ↑v / -Real.log ↑u) ^ (1 / ν)))))

Table 1: the t-EV CDF at interior points.

theorem Papers.AnsariRockel2024.tEV_isCI (ν r : ℝ) (hν : 0 < ν) (hr : r ∈ Set.Icc (-1) 1) : (Verification.tEV ν r hν hr).IsCI

Table 5: the t-EV copula is CI for every admissible parameter.

theorem Papers.AnsariRockel2024.tEV_extremalCoefficient (ν r : ℝ) (hν : 0 < ν) (hr : r ∈ Set.Ioo (-1) 1) : (Verification.tEV ν r hν ⋯).extremalCoefficient = 2 * Verification.studentTCDF (ν + 1) √((ν + 1) * (1 - r) / (1 + r))

The extremal coefficient 2 T_{ν+1}(z_{1/2}), with z_{1/2}=sqrt((ν+1)(1-ρ)/(1+ρ)).

theorem Papers.AnsariRockel2024.tEV_tails (ν r : ℝ) (hν : 0 < ν) (hr : r ∈ Set.Ioo (-1) 1) : (Verification.tEV ν r hν ⋯).HasLowerTailDependence 0 ∧ (Verification.tEV ν r hν ⋯).HasUpperTailDependence (2 * (1 - Verification.studentTCDF (ν + 1) √((ν + 1) * (1 - r) / (1 + r))))

Table 5: lower tail zero and upper tail 2(1-T_{ν+1}(z_{1/2})) for -1<ρ<1.

theorem Papers.AnsariRockel2024.tEV_one (ν : ℝ) (hν : 0 < ν) : Verification.tEV ν 1 hν ⋯ = ProbabilityTheory.Copula.comonotonic 2

The correlation endpoint ρ=1 is the comonotonic copula; in particular the lower tail coefficient is 1{ρ=1} across the closed range.

theorem Papers.AnsariRockel2024.tEV_negative_one (ν : ℝ) (hν : 0 < ν) : Verification.tEV ν (-1) hν ⋯ = ProbabilityTheory.Copula.independence 2

theorem Papers.AnsariRockel2024.tEV_lowerTail (ν r : ℝ) (hν : 0 < ν) (hr : r ∈ Set.Ioc (-1) 1) : (Verification.tEV ν r hν ⋯).HasLowerTailDependence (if r = 1 then 1 else 0)

theorem Papers.AnsariRockel2024.tEV_lowerOrthant_mono (ν r q : ℝ) (hν : 0 < ν) (hr : r ∈ Set.Ioo (-1) 1) (hq : q ∈ Set.Ioo (-1) 1) (hrq : r ≤ q) : (Verification.tEV ν r hν ⋯).LowerOrthantLE (Verification.tEV ν q hν ⋯)

theorem Papers.AnsariRockel2024.tEV_schurBoth_mono (ν r q : ℝ) (hν : 0 < ν) (hr : r ∈ Set.Ioo (-1) 1) (hq : q ∈ Set.Ioo (-1) 1) (hrq : r ≤ q) : (Verification.tEV ν r hν ⋯).SchurBothLE (Verification.tEV ν q hν ⋯)

theorem Papers.AnsariRockel2024.tEV_lowerOrthant_iff (ν r q : ℝ) (hν : 0 < ν) (hr : r ∈ Set.Ioo (-1) 1) (hq : q ∈ Set.Ioo (-1) 1) : (Verification.tEV ν r hν ⋯).LowerOrthantLE (Verification.tEV ν q hν ⋯) ↔ r ≤ q

Table 5: the lower-orthant order is exactly the correlation order on (-1,1).

theorem Papers.AnsariRockel2024.tEV_schurBoth_iff (ν r q : ℝ) (hν : 0 < ν) (hr : r ∈ Set.Ioo (-1) 1) (hq : q ∈ Set.Ioo (-1) 1) : (Verification.tEV ν r hν ⋯).SchurBothLE (Verification.tEV ν q hν ⋯) ↔ r ≤ q

Table 5: the two-direction Schur order is exactly the correlation order on (-1,1).

theorem Papers.AnsariRockel2024.tEV_closed_lowerOrthant_mono (ν r q : ℝ) (hν : 0 < ν) (hr : r ∈ Set.Icc (-1) 1) (hq : q ∈ Set.Icc (-1) 1) (hrq : r ≤ q) : (Verification.tEV ν r hν hr).LowerOrthantLE (Verification.tEV ν q hν hq)

Increasing lower-orthant order on the closed correlation interval, including the independence and comonotonic endpoints.

theorem Papers.AnsariRockel2024.tEV_closed_schurBoth_mono (ν r q : ℝ) (hν : 0 < ν) (hr : r ∈ Set.Icc (-1) 1) (hq : q ∈ Set.Icc (-1) 1) (hrq : r ≤ q) : (Verification.tEV ν r hν hr).SchurBothLE (Verification.tEV ν q hν hq)