← Mathematical handbook

The t-EV Pickands function in Student-t form

For -1<r<1 and ν>0, the spectral t-EV construction of TEVConstruction.lean has stable tail function L(x,y)=x T_{ν+1}(k((x/y)^(1/ν)-r))+y T_{ν+1}(k((y/x)^(1/ν)-r)), k=sqrt((1+ν)/(1-r²)), for positive x,y. Consequently its Pickands function is the expression printed in Tables 1 and 4 of Ansari–Rockel.

Two Gaussian representations

noncomputable def Verification.gaussianMixSwap (r : ℝ) : EuclideanSpace ℝ (Fin 2) →L[ℝ] EuclideanSpace ℝ (Fin 2)

Equations

• Verification.gaussianMixSwap r = ↑(EuclideanSpace.equiv (Fin 2) ℝ).symm ∘SL ContinuousLinearMap.pi ![r • EuclideanSpace.proj 0 + √(1 - r ^ 2) • EuclideanSpace.proj 1, EuclideanSpace.proj 0]

noncomputable def Verification.gaussianMixSwapRow (r : ℝ) (i : Fin 2) : EuclideanSpace ℝ (Fin 2)

Equations

• Verification.gaussianMixSwapRow r i = WithLp.toLp 2 (!![r, √(1 - r ^ 2); 1, 0] i)

theorem Verification.gaussianMixSwap_inner (r : ℝ) (i : Fin 2) : (fun (u : EuclideanSpace ℝ (Fin 2)) => inner ℝ ((EuclideanSpace.basisFun (Fin 2) ℝ).toBasis i) u) ∘ ⇑(gaussianMixSwap r) = fun (u : EuclideanSpace ℝ (Fin 2)) => inner ℝ (gaussianMixSwapRow r i) u

theorem Verification.map_gaussianMixSwap {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) : MeasureTheory.Measure.map (⇑(gaussianMixSwap r)) (ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin 2))) = ProbabilityTheory.multivariateGaussian 0 (bivariateCorrelation r)

theorem Verification.integral_bivariateGaussian_mix {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (F : ℝ → ℝ → ℝ) (hF : Measurable (Function.uncurry F)) : ∫ (z : EuclideanSpace ℝ (Fin 2)), F (z.ofLp 0) (z.ofLp 1) ∂ProbabilityTheory.multivariateGaussian 0 (bivariateCorrelation r) = ∫ (p : ℝ × ℝ), F p.1 (r * p.1 + √(1 - r ^ 2) * p.2) ∂(ProbabilityTheory.gaussianReal 0 1).prod (ProbabilityTheory.gaussianReal 0 1)

theorem Verification.integral_bivariateGaussian_mixSwap {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (F : ℝ → ℝ → ℝ) (hF : Measurable (Function.uncurry F)) : ∫ (z : EuclideanSpace ℝ (Fin 2)), F (z.ofLp 0) (z.ofLp 1) ∂ProbabilityTheory.multivariateGaussian 0 (bivariateCorrelation r) = ∫ (p : ℝ × ℝ), F (r * p.1 + √(1 - r ^ 2) * p.2) p.1 ∂(ProbabilityTheory.gaussianReal 0 1).prod (ProbabilityTheory.gaussianReal 0 1)

Pointwise threshold identities

theorem Verification.gaussianPositiveWeight_le_iff (ν : ℝ) (hν : 0 < ν) {κ a : ℝ} (hκ : 0 < κ) (ha : 0 < a) (z : ℝ) : gaussianPositiveWeight ν z ≤ κ * gaussianPositiveWeight ν a ↔ z ≤ κ ^ (1 / ν) * a

theorem Verification.gaussianPositiveWeight_lt_iff (ν : ℝ) (hν : 0 < ν) {κ a : ℝ} (hκ : 0 < κ) (ha : 0 < a) (z : ℝ) : gaussianPositiveWeight ν z < κ * gaussianPositiveWeight ν a ↔ z < κ ^ (1 / ν) * a

theorem Verification.gaussianPositiveWeight_of_nonpos (ν : ℝ) (hν : 0 < ν) {a : ℝ} (ha : a ≤ 0) : gaussianPositiveWeight ν a = 0

theorem Verification.standardGaussian_linear_halfline_strict {s : ℝ} (hs : 0 < s) (b : ℝ) : ∫ (y : ℝ), if s * y < b then 1 else 0 ∂ProbabilityTheory.gaussianReal 0 1 = ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) (b / s)

Conditional evaluation

theorem Verification.tEV_weighted_normalCDF (ν : ℝ) (hν : 0 < ν) (q : ℝ) : ∫ (a : ℝ), gaussianPositiveWeight ν a * ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) (q * a) ∂ProbabilityTheory.gaussianReal 0 1 = studentTCDF (ν + 1) (q * √(ν + 1))

theorem Verification.integrable_weight_indicator (ν : ℝ) (hν : 0 < ν) (P : ℝ × ℝ → Prop) [DecidablePred P] (hP : MeasurableSet {p : ℝ × ℝ | P p}) : MeasureTheory.Integrable (fun (p : ℝ × ℝ) => gaussianPositiveWeight ν p.1 * if P p then 1 else 0) ((ProbabilityTheory.gaussianReal 0 1).prod (ProbabilityTheory.gaussianReal 0 1))

theorem Verification.tEV_threshold_le (ν r : ℝ) (hν : 0 < ν) (hr : r ∈ Set.Ioo (-1) 1) {κ : ℝ} (hκ : 0 < κ) : ∫ (p : ℝ × ℝ), gaussianPositiveWeight ν p.1 * if gaussianPositiveWeight ν (r * p.1 + √(1 - r ^ 2) * p.2) ≤ κ * gaussianPositiveWeight ν p.1 then 1 else 0 ∂(ProbabilityTheory.gaussianReal 0 1).prod (ProbabilityTheory.gaussianReal 0 1) = studentTCDF (ν + 1) ((κ ^ (1 / ν) - r) / √(1 - r ^ 2) * √(ν + 1))

The conditional threshold integral with a non-strict comparison.

theorem Verification.tEV_threshold_lt (ν r : ℝ) (hν : 0 < ν) (hr : r ∈ Set.Ioo (-1) 1) {κ : ℝ} (hκ : 0 < κ) : ∫ (p : ℝ × ℝ), gaussianPositiveWeight ν p.1 * if gaussianPositiveWeight ν (r * p.1 + √(1 - r ^ 2) * p.2) < κ * gaussianPositiveWeight ν p.1 then 1 else 0 ∂(ProbabilityTheory.gaussianReal 0 1).prod (ProbabilityTheory.gaussianReal 0 1) = studentTCDF (ν + 1) ((κ ^ (1 / ν) - r) / √(1 - r ^ 2) * √(ν + 1))

The conditional threshold integral with a strict comparison.

The stable tail function

noncomputable def Verification.tEVArg (ν r s : ℝ) : ℝ

The argument z of the t-EV Pickands function, written for a ratio s.

Equations

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

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

theorem Verification.tEVStableTail_formula (ν r : ℝ) (hν : 0 < ν) (hr : r ∈ Set.Ioo (-1) 1) {x y : ℝ} (hx : 0 < x) (hy : 0 < y) : (tEVStableTail ν r hν ⋯).value x y = x * studentTCDF (ν + 1) (tEVArg ν r ((x / y) ^ (1 / ν))) + y * studentTCDF (ν + 1) (tEVArg ν r ((y / x) ^ (1 / ν)))

theorem Verification.tEV_pickands_formula (ν r : ℝ) (hν : 0 < ν) (hr : r ∈ Set.Ioo (-1) 1) (t : ↑unitInterval) (ht : ↑t ∈ Set.Ioo 0 1) : copulaPickands (tEV ν r hν ⋯) t = (1 - ↑t) * studentTCDF (ν + 1) (tEVArg ν r (((1 - ↑t) / ↑t) ^ (1 / ν))) + ↑t * studentTCDF (ν + 1) (tEVArg ν r ((↑t / (1 - ↑t)) ^ (1 / ν)))

The t-EV Pickands function on the open unit interval, as printed in Tables 1 and 4.

theorem Verification.tEV_cdf_interior (ν r : ℝ) (hν : 0 < ν) (hr : r ∈ Set.Ioo (-1) 1) (u v : ↑unitInterval) (hu : ↑u ∈ Set.Ioo 0 1) (hv : ↑v ∈ Set.Ioo 0 1) : (tEV ν r hν ⋯).cdf ![u, v] = Real.exp (-(-Real.log ↑u * studentTCDF (ν + 1) (tEVArg ν r ((-Real.log ↑u / -Real.log ↑v) ^ (1 / ν))) + -Real.log ↑v * studentTCDF (ν + 1) (tEVArg ν r ((-Real.log ↑v / -Real.log ↑u) ^ (1 / ν)))))

The t-EV CDF at interior points, as an extreme-value copula with the Student-t stable tail function.