Degrees-of-freedom limit of the t-EV family #
For a fixed correlation -1<r<1, the t-EV copulas converge pointwise to the independence
copula as ν → ∞. In particular the Hüsler–Reiss family is not the fixed-correlation limit.
theorem
Verification.studentTCDF_lower_bound
(k : ℝ)
(hk : 0 < k)
{z : ℝ}
(hz : 0 ≤ z)
:
↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) (z / 2) * (1 - (k / 2)⁻¹ / (3 / 4) ^ 2) ≤ studentTCDF k z
theorem
Verification.studentTCDF_tendsto_one
{ι : Type u_1}
{l : Filter ι}
(k z : ι → ℝ)
(hk : ∀ (i : ι), 0 < k i)
(hkt : Filter.Tendsto k l Filter.atTop)
(hzt : Filter.Tendsto z l Filter.atTop)
:
Filter.Tendsto (fun (i : ι) => studentTCDF (k i) (z i)) l (nhds 1)
theorem
Verification.tEVArg_tendsto_atTop
{ι : Type u_1}
{l : Filter ι}
(ν : ι → ℝ)
(_hν : ∀ (i : ι), 0 < ν i)
(hνt : Filter.Tendsto ν l Filter.atTop)
{r : ℝ}
(hr : r ∈ Set.Ioo (-1) 1)
{c : ℝ}
(hc : 0 < c)
:
Filter.Tendsto (fun (i : ι) => tEVArg (ν i) r (c ^ (1 / ν i))) l Filter.atTop
theorem
Verification.tEV_tendsto_independence
{ι : Type u_1}
{l : Filter ι}
(ν : ι → ℝ)
(hν : ∀ (i : ι), 0 < ν i)
(hνt : Filter.Tendsto ν l Filter.atTop)
{r : ℝ}
(hr : r ∈ Set.Ioo (-1) 1)
(u v : ↑unitInterval)
:
Table 4 audit: for fixed ρ∈(-1,1), the t-EV copula tends to independence as ν → ∞
(pointwise on the closed square).