← Mathematical handbook

theorem Verification.bivariateGaussian_eval_preserving (r : ℝ) (hr : r ∈ Set.Icc (-1) 1) (i : Fin 2) : MeasureTheory.MeasurePreserving (fun (z : EuclideanSpace ℝ (Fin 2)) => z.ofLp i) (ProbabilityTheory.multivariateGaussian 0 (bivariateCorrelation r)) (ProbabilityTheory.gaussianReal 0 1)

theorem Verification.gaussianPositiveWeight_coordinate_integrable (ν r : ℝ) (hν : 0 < ν) (hr : r ∈ Set.Icc (-1) 1) (i : Fin 2) : MeasureTheory.Integrable (fun (z : EuclideanSpace ℝ (Fin 2)) => gaussianPositiveWeight ν (z.ofLp i)) (ProbabilityTheory.multivariateGaussian 0 (bivariateCorrelation r))

theorem Verification.gaussianPositiveWeight_coordinate_mean (ν r : ℝ) (hν : 0 < ν) (hr : r ∈ Set.Icc (-1) 1) (i : Fin 2) : ∫ (z : EuclideanSpace ℝ (Fin 2)), gaussianPositiveWeight ν (z.ofLp i) ∂ProbabilityTheory.multivariateGaussian 0 (bivariateCorrelation r) = 1

noncomputable def Verification.tEVStableTail (ν r : ℝ) (hν : 0 < ν) (hr : r ∈ Set.Icc (-1) 1) : StableTail

Equations

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

noncomputable def Verification.tEV (ν r : ℝ) (hν : 0 < ν) (hr : r ∈ Set.Icc (-1) 1) : ProbabilityTheory.Copula 2

Equations

• Verification.tEV ν r hν hr = Verification.stableTailCopula (Verification.tEVStableTail ν r hν hr)

theorem Verification.tEV_isExtremeValue (ν r : ℝ) (hν : 0 < ν) (hr : r ∈ Set.Icc (-1) 1) : (tEV ν r hν hr).IsExtremeValue

theorem Verification.tEV_isCI (ν r : ℝ) (hν : 0 < ν) (hr : r ∈ Set.Icc (-1) 1) : (tEV ν r hν hr).IsCI

theorem Verification.tEV_pickands_spectral (ν r : ℝ) (hν : 0 < ν) (hr : r ∈ Set.Icc (-1) 1) (t : ↑unitInterval) : copulaPickands (tEV ν r hν hr) t = ∫ (z : EuclideanSpace ℝ (Fin 2)), max ((1 - ↑t) * gaussianPositiveWeight ν (z.ofLp 0)) (↑t * gaussianPositiveWeight ν (z.ofLp 1)) ∂ProbabilityTheory.multivariateGaussian 0 (bivariateCorrelation r)