Documentation

Verification.GumbelDensity

← Mathematical handbook

noncomputable def Verification.gumbelInv (θ u : ℝ) :

Equations

Verification.gumbelInv θ u = (-Real.log u) ^ θ

Instances For

noncomputable def Verification.gumbelWeight (θ u : ℝ) :

Equations

Verification.gumbelWeight θ u = θ * (-Real.log u) ^ (θ - 1) / u

Instances For

noncomputable def Verification.gumbelDensityReal (θ u v : ℝ) :

Equations

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

Instances For

noncomputable def Verification.gumbelDensity (θ : ℝ) (x : Fin 2 → ↑unitInterval) :

Equations

Verification.gumbelDensity θ x = Verification.gumbelDensityReal θ ↑(x 0) ↑(x 1)

Instances For

noncomputable def Verification.gumbelPartial (θ u v : ℝ) :

Equations

Verification.gumbelPartial θ u v = -Verification.gumbelPsiDeriv θ⁻¹ (Verification.gumbelInv θ u + Verification.gumbelInv θ v) * Verification.gumbelWeight θ u

Instances For

noncomputable def Verification.gumbelRealCDF (θ u v : ℝ) :

Equations

Verification.gumbelRealCDF θ u v = Real.exp (-(Verification.gumbelInv θ u + Verification.gumbelInv θ v) ^ θ⁻¹)

Instances For

theorem Verification.gumbelInv_pos {θ u : ℝ} (hu : u ∈ Set.Ioo 0 1) :

0 < gumbelInv θ u

theorem Verification.gumbelWeight_pos {θ u : ℝ} (hθ : 0 < θ) (hu : u ∈ Set.Ioo 0 1) :

0 < gumbelWeight θ u

theorem Verification.gumbelInv_deriv {θ u : ℝ} (hu : u ∈ Set.Ioo 0 1) :

HasDerivAt (gumbelInv θ) (-gumbelWeight θ u) u

theorem Verification.gumbelWeight_continuousAt {θ u : ℝ} (hu : u ∈ Set.Ioo 0 1) :

ContinuousAt (gumbelWeight θ) u

theorem Verification.gumbelSecond_continuousAt {p t : ℝ} (ht : 0 < t) :

ContinuousAt (gumbelSecond p) t

theorem Verification.gumbelPartial_deriv {θ u v : ℝ} (hu : u ∈ Set.Ioo 0 1) (hv : v ∈ Set.Ioo 0 1) :

HasDerivAt (gumbelPartial θ u) (gumbelDensityReal θ u v) v

theorem Verification.gumbelRealCDF_deriv {θ u v : ℝ} (hu : u ∈ Set.Ioo 0 1) (hv : v ∈ Set.Ioo 0 1) :

HasDerivAt (fun (x : ℝ) => gumbelRealCDF θ x v) (gumbelPartial θ u v) u

theorem Verification.gumbelDensity_measurable (θ : ℝ) :

Measurable (gumbelDensity θ)

theorem Verification.gumbelDensityReal_nonneg {θ : ℝ} (hθ : 1 ≤ θ) (u v : ℝ) :

0 ≤ gumbelDensityReal θ u v

theorem Verification.gumbelDensityReal_continuousAt {θ u v : ℝ} (hu : u ∈ Set.Ioo 0 1) (hv : v ∈ Set.Ioo 0 1) :

ContinuousAt (Function.uncurry (gumbelDensityReal θ)) (u, v)

theorem Verification.gumbelPartial_continuousAt {θ u v : ℝ} (hu : u ∈ Set.Ioo 0 1) (hv : v ∈ Set.Ioo 0 1) :

ContinuousAt (fun (x : ℝ) => gumbelPartial θ x v) u

theorem Verification.gumbel_toMeasure_density {θ : ℝ} (hθ : 1 ≤ θ) :

(ProbabilityTheory.Copula.gumbel θ hθ).toMeasure = MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal (gumbelDensity θ x)

theorem Verification.gumbelDensity_mtp2 {θ : ℝ} (hθ : 1 ≤ θ) :

ProbabilityTheory.IsMTP2 (gumbelDensity θ)

theorem Verification.gumbel_hasMTP2Density {θ : ℝ} (hθ : 1 ≤ θ) :

(ProbabilityTheory.Copula.gumbel θ hθ).HasMTP2Density