← Mathematical handbook

The t-EV copula at ν=1, r=0

With two degrees of freedom the Student-t CDF is T₂(z)=1/2+z/(2√(2+z²)). At ν=1, r=0 the t-EV stable tail function becomes (x+y+√(x²+y²))/2, i.e. the Tawn copula with θ=2, α=β=1/2. On Pythagorean powers u=t^m, v=t^n (m²+n²=s²) the CDF is t^((m+n+s)/2), and the same rectangle witness as for Tawn excludes a TP2 density.

noncomputable def Verification.studentT2Closed (z : ℝ) : ℝ

Equations

• Verification.studentT2Closed z = 1 / 2 + z / (2 * √(2 + z ^ 2))

theorem Verification.studentMarginalPDF_two (z : ℝ) : studentMarginalPDF 2 z = 1 / √(2 + z ^ 2) ^ 3

theorem Verification.hasDerivAt_studentT2Closed (z : ℝ) : HasDerivAt studentT2Closed (1 / √(2 + z ^ 2) ^ 3) z

theorem Verification.studentTCDF_two (z : ℝ) : studentTCDF 2 z = studentT2Closed z

The two-degree-of-freedom Student-t CDF in closed form.

theorem Verification.tEV_one_zero_cdf_pow {t : ℝ} (ht0 : 0 < t) (ht1 : t < 1) (m n s e : ℕ) (hm : 0 < m) (hn : 0 < n) (hs : m ^ 2 + n ^ 2 = s ^ 2) (he : m + n + s = 2 * e) (u v : ↑unitInterval) (hu : ↑u = t ^ m) (hv : ↑v = t ^ n) : (tEV 1 0 ⋯ ⋯).cdf ![u, v] = t ^ e

The ν=1, r=0 t-EV CDF on Pythagorean powers of t∈(0,1).