← Mathematical handbook

The ν → 0 limit of the t-EV family

The Student-t CDF with one degree of freedom is the Cauchy CDF 1/2+arctan(x)/π, and T_k → T_1 locally uniformly in the argument as k → 1. Consequently the t-EV copulas converge, as ν → 0+, to the Marshall–Olkin copula with equal weights α=β=1/2+arcsin(ρ)/π.

theorem Verification.studentMarginalPDF_one (x : ℝ) : studentMarginalPDF 1 x = 1 / (Real.pi * (1 + x ^ 2))

theorem Verification.studentTCDF_one (x : ℝ) : studentTCDF 1 x = 1 / 2 + Real.arctan x / Real.pi

The Cauchy CDF.

noncomputable def Verification.studentConst (k : ℝ) : ℝ

Normalizing constant of the Student density.

Equations

• Verification.studentConst k = Real.Gamma ((k + 1) / 2) / (√(k * Real.pi) * Real.Gamma (k / 2))

theorem Verification.studentConst_continuousOn : ContinuousOn studentConst (Set.Icc 1 2)

theorem Verification.studentConst_bound : ∃ (M : ℝ), 0 < M ∧ ∀ k ∈ Set.Icc 1 2, studentConst k ≤ M

theorem Verification.studentMarginalPDF_le {k : ℝ} (hk : k ∈ Set.Icc 1 2) {M : ℝ} (hM : studentConst k ≤ M) (t : ℝ) : studentMarginalPDF k t ≤ 2 * M / (1 + t ^ 2)

theorem Verification.studentMarginalPDF_continuousAt_df (t : ℝ) {k : ℝ} (hk : 0 < k) : ContinuousAt (fun (k : ℝ) => studentMarginalPDF k t) k

theorem Verification.studentTCDF_eq_integral_indicator (k : ℝ) (hk : 0 < k) (x : ℝ) : studentTCDF k x = ∫ (t : ℝ), (Set.Iic x).indicator (studentMarginalPDF k) t

theorem Verification.studentTCDF_tendsto_df {ι : Type u_1} {l : Filter ι} [l.IsCountablyGenerated] (k x : ι → ℝ) (hk : ∀ (i : ι), k i ∈ Set.Icc 1 2) (hkl : Filter.Tendsto k l (nhds 1)) {x0 : ℝ} (hx : Filter.Tendsto x l (nhds x0)) : Filter.Tendsto (fun (i : ι) => studentTCDF (k i) (x i)) l (nhds (studentTCDF 1 x0))

Continuity of T_k(x) in (k,x) at k=1.

theorem Verification.studentTCDF_tendsto_df_atTop {ι : Type u_1} {l : Filter ι} [l.IsCountablyGenerated] (k x : ι → ℝ) (hk : ∀ (i : ι), k i ∈ Set.Icc 1 2) (hkl : Filter.Tendsto k l (nhds 1)) (hx : Filter.Tendsto x l Filter.atTop) : Filter.Tendsto (fun (i : ι) => studentTCDF (k i) (x i)) l (nhds 1)

T_k(x)→1 as k→1 and x→∞.

theorem Verification.arctan_tEV_half {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) : Real.arctan (√(1 - r ^ 2) / (1 + r)) = Real.pi / 4 - Real.arcsin r / 2

theorem Verification.tEVArg_one_zero_limit {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) : √((1 + 0) / (1 - r ^ 2)) * (1 - r) = √(1 - r ^ 2) / (1 + r)

noncomputable def Verification.tEVZeroWeight (r : ℝ) : ℝ

The common Marshall–Olkin weight of the ν → 0 limit.

Equations

• Verification.tEVZeroWeight r = 1 / 2 + Real.arcsin r / Real.pi

theorem Verification.tEVZeroWeight_mem (r : ℝ) : tEVZeroWeight r ∈ Set.Icc 0 1

noncomputable def Verification.tEVZeroWeightI (r : ℝ) : ↑unitInterval

Equations

• Verification.tEVZeroWeightI r = ⟨Verification.tEVZeroWeight r, ⋯⟩

theorem Verification.marshallOlkin_equal_exp (a : ↑unitInterval) {x y : ℝ} (hx : 0 < x) (hy : 0 < y) : (ProbabilityTheory.Copula.marshallOlkin a a).cdf ![⟨Real.exp (-x), ⋯⟩, ⟨Real.exp (-y), ⋯⟩] = Real.exp (-(max x y + (1 - ↑a) * min x y))

Marshall–Olkin with equal weights in exponential coordinates.

theorem Verification.studentTCDF_one_neg_arcsin {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) : studentTCDF 1 (√((1 + 0) / (1 - r ^ 2)) * (0 - r)) = 1 - tEVZeroWeight r

theorem Verification.studentTCDF_one_half_limit {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) : studentTCDF 1 (√((1 + 0) / (1 - r ^ 2)) * (1 - r)) = 1 - tEVZeroWeight r / 2

theorem Verification.tEVArg_zero_limit_finite {ι : Type u_1} {l : Filter ι} (ν : ι → ℝ) (hνl : Filter.Tendsto ν l (nhds 0)) (r : ℝ) {w : ι → ℝ} {w0 : ℝ} (hw : Filter.Tendsto w l (nhds w0)) : Filter.Tendsto (fun (i : ι) => tEVArg (ν i) r (w i)) l (nhds (√((1 + 0) / (1 - r ^ 2)) * (w0 - r)))

theorem Verification.tEVArg_zero_limit_atTop {ι : Type u_1} {l : Filter ι} (ν : ι → ℝ) (hνl : Filter.Tendsto ν l (nhds 0)) {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) {w : ι → ℝ} (hw : Filter.Tendsto w l Filter.atTop) : Filter.Tendsto (fun (i : ι) => tEVArg (ν i) r (w i)) l Filter.atTop

theorem Verification.tEV_tendsto_marshallOlkin {ι : Type u_1} {l : Filter ι} [l.IsCountablyGenerated] (ν : ι → ℝ) (hν : ∀ (i : ι), 0 < ν i) (hν1 : ∀ (i : ι), ν i ≤ 1) (hνl : Filter.Tendsto ν l (nhds 0)) {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) (u v : ↑unitInterval) : Filter.Tendsto (fun (i : ι) => (tEV (ν i) r ⋯ ⋯).cdf ![u, v]) l (nhds ((ProbabilityTheory.Copula.marshallOlkin (tEVZeroWeightI r) (tEVZeroWeightI r)).cdf ![u, v]))

Table 4 audit: as ν → 0+, the t-EV copula tends pointwise to the Marshall–Olkin copula with equal weights 1/2+arcsin(ρ)/π.