← Mathematical handbook

Monotonicity of the t-EV family in the correlation parameter

The Pickands function of the t-EV copula decreases in r on (-1,1). The derivative of the two Student-t terms is -K t f(z_t) (w²-2rw+1) with K>0, where the balance identity (1-t) f(z_{1-t}) = t w² f(z_t) relates the two Student-t densities.

theorem Verification.tEVArg_eq_div (ν r w : ℝ) (hν : 0 < ν) : tEVArg ν r w = √(1 + ν) * ((w - r) / √(1 - r ^ 2))

noncomputable def Verification.tEVArgDeriv (ν r w : ℝ) : ℝ

Derivative of the Pickands argument in the correlation parameter.

Equations

• Verification.tEVArgDeriv ν r w = √(1 + ν) * ((r * w - 1) / ((1 - r ^ 2) * √(1 - r ^ 2)))

theorem Verification.tEVArg_hasDerivAt (ν w : ℝ) (hν : 0 < ν) {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) : HasDerivAt (fun (q : ℝ) => tEVArg ν q w) (tEVArgDeriv ν r w) r

theorem Verification.tEVArg_sq (ν r w : ℝ) (hν : 0 < ν) (hr : r ∈ Set.Ioo (-1) 1) : tEVArg ν r w ^ 2 = (1 + ν) / (1 - r ^ 2) * (w - r) ^ 2

theorem Verification.tEV_density_balance (ν r w : ℝ) (hν : 0 < ν) (hr : r ∈ Set.Ioo (-1) 1) (hw : 0 < w) : studentMarginalPDF (ν + 1) (tEVArg ν r w⁻¹) = (w ^ 2) ^ ((ν + 1) / 2 + 1 / 2) * studentMarginalPDF (ν + 1) (tEVArg ν r w)

Balance identity of the Student-t densities at the two Pickands arguments.

noncomputable def Verification.tEVPickandsExpr (ν r t : ℝ) : ℝ

The Pickands expression for fixed t, as a function of the correlation.

Equations

• One or more equations did not get rendered due to their size.

theorem Verification.tEVPickandsExpr_hasDerivAt (ν t : ℝ) (hν : 0 < ν) (_ht : t ∈ Set.Ioo 0 1) {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) : HasDerivAt (fun (q : ℝ) => tEVPickandsExpr ν q t) ((1 - t) * (studentMarginalPDF (ν + 1) (tEVArg ν r (((1 - t) / t) ^ (1 / ν))) * tEVArgDeriv ν r (((1 - t) / t) ^ (1 / ν))) + t * (studentMarginalPDF (ν + 1) (tEVArg ν r ((t / (1 - t)) ^ (1 / ν))) * tEVArgDeriv ν r ((t / (1 - t)) ^ (1 / ν)))) r

theorem Verification.tEVPickandsExpr_deriv_nonpos (ν t : ℝ) (hν : 0 < ν) (ht : t ∈ Set.Ioo 0 1) {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) : (1 - t) * (studentMarginalPDF (ν + 1) (tEVArg ν r (((1 - t) / t) ^ (1 / ν))) * tEVArgDeriv ν r (((1 - t) / t) ^ (1 / ν))) + t * (studentMarginalPDF (ν + 1) (tEVArg ν r ((t / (1 - t)) ^ (1 / ν))) * tEVArgDeriv ν r ((t / (1 - t)) ^ (1 / ν))) ≤ 0

theorem Verification.tEVPickandsExpr_antitoneOn (ν t : ℝ) (hν : 0 < ν) (ht : t ∈ Set.Ioo 0 1) : AntitoneOn (fun (r : ℝ) => tEVPickandsExpr ν r t) (Set.Ioo (-1) 1)

theorem Verification.tEV_pickands_eq_expr (ν r : ℝ) (hν : 0 < ν) (hr : r ∈ Set.Ioo (-1) 1) (t : ↑unitInterval) (ht : ↑t ∈ Set.Ioo 0 1) : copulaPickands (tEV ν r hν ⋯) t = tEVPickandsExpr ν r ↑t

theorem Verification.tEV_pickands_antitone (ν r q : ℝ) (hν : 0 < ν) (hr : r ∈ Set.Ioo (-1) 1) (hq : q ∈ Set.Ioo (-1) 1) (hrq : r ≤ q) (t : ↑unitInterval) (ht : ↑t ∈ Set.Ioo 0 1) : copulaPickands (tEV ν q hν ⋯) t ≤ copulaPickands (tEV ν r hν ⋯) t

Diagonal, extremal coefficient and tails

theorem Verification.tEVArg_one (ν r : ℝ) (hν : 0 < ν) (hr : r ∈ Set.Ioo (-1) 1) : tEVArg ν r 1 = √((ν + 1) * (1 - r) / (1 + r))

theorem Verification.tEVArg_one_pos (ν r : ℝ) (hν : 0 < ν) (hr : r ∈ Set.Ioo (-1) 1) : 0 < tEVArg ν r 1

theorem Verification.tEVArg_one_strictAntiOn (ν : ℝ) (hν : 0 < ν) : StrictAntiOn (fun (r : ℝ) => tEVArg ν r 1) (Set.Ioo (-1) 1)

theorem Verification.tEV_pickands_half (ν r : ℝ) (hν : 0 < ν) (hr : r ∈ Set.Ioo (-1) 1) : copulaPickands (tEV ν r hν ⋯) ProbabilityTheory.Copula.unitHalf = studentTCDF (ν + 1) (tEVArg ν r 1)

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

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