← Mathematical handbook

Singular correlation endpoints of the t-EV construction

At r=1 the Gaussian coordinates coincide and the construction is the comonotonic copula. At r=-1 the positive parts have disjoint supports and it is the independence copula.

theorem Verification.tEV_one_pickands_half (ν : ℝ) (hν : 0 < ν) : copulaPickands (tEV ν 1 hν ⋯) ProbabilityTheory.Copula.unitHalf = 1 / 2

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

theorem Verification.gaussianPositiveWeight_neg_mean (ν : ℝ) (hν : 0 < ν) : ∫ (z : ℝ), gaussianPositiveWeight ν (-z) ∂ProbabilityTheory.gaussianReal 0 1 = 1

theorem Verification.tEVStableTail_negative_one (ν : ℝ) (hν : 0 < ν) {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) : (tEVStableTail ν (-1) hν ⋯).value x y = x + y

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