← Mathematical handbook

noncomputable def Verification.lognormalSpectralWeight (s z : ℝ) : ℝ

Equations

• Verification.lognormalSpectralWeight s z = Real.exp (s * z - s ^ 2 / 2)

theorem Verification.lognormalSpectralWeight_integrable (s : ℝ) : MeasureTheory.Integrable (lognormalSpectralWeight s) (ProbabilityTheory.gaussianReal 0 1)

theorem Verification.lognormalSpectralWeight_mean (s : ℝ) : ∫ (z : ℝ), lognormalSpectralWeight s z ∂ProbabilityTheory.gaussianReal 0 1 = 1

noncomputable def Verification.huslerReissStableTail (δ : ℝ) : StableTail

Equations

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

noncomputable def Verification.huslerReissPositive (δ : ℝ) (_hδ : 0 < δ) : ProbabilityTheory.Copula 2

The positive-parameter Hüsler–Reiss spectral construction. The paper's explicit Gaussian-CDF formula is identified in HuslerReissFormula.lean.

Equations

• Verification.huslerReissPositive δ _hδ = Verification.stableTailCopula (Verification.huslerReissStableTail δ)

theorem Verification.huslerReissPositive_isExtremeValue (δ : ℝ) (hδ : 0 < δ) : (huslerReissPositive δ hδ).IsExtremeValue

theorem Verification.huslerReissPositive_isCI (δ : ℝ) (hδ : 0 < δ) : (huslerReissPositive δ hδ).IsCI

theorem Verification.huslerReissPositive_pickands_spectral (δ : ℝ) (hδ : 0 < δ) (t : ↑unitInterval) : copulaPickands (huslerReissPositive δ hδ) t = ∫ (z : ℝ), max ((1 - ↑t) * Real.exp (2 / δ * z - (2 / δ) ^ 2 / 2)) ↑t ∂ProbabilityTheory.gaussianReal 0 1