Gumbel distributions over ℝ

The Gumbel distribution with location μ and scale β, the type I extreme value distribution, has distribution function exp (-exp (-((x - μ) / β))). Like gaussianReal and cauchyMeasure, the measure takes its scale in ℝ≥0 and is dirac μ at scale zero. The family is max-stable: the maximum of independent Gumbel variables of a common scale is Gumbel with that scale. [UPSTREAM] candidate for Mathlib/Probability/Distributions/Gumbel.lean.

Main definitions

• gumbelPDFReal: the function μ β x ↦ β⁻¹ * exp (-((x - μ) / β)) * exp (-exp (-((x - μ) / β))), the probability density function of the Gumbel distribution with location μ and scale β (when β ≠ 0).
• gumbelPDF: ℝ≥0∞-valued pdf, gumbelPDF μ β x = ENNReal.ofReal (gumbelPDFReal μ β x).
• gumbelMeasure: the Gumbel measure on ℝ. If β = 0 it is dirac μ, otherwise the measure with density gumbelPDF μ β with respect to the Lebesgue measure.

Main results

• cdf_gumbelMeasure_eq: the cdf is exp (-exp (-((x - μ) / β))).
• gumbelPDFReal_eq_mul_cdf: the pdf is the cdf times the reverse hazard rate β⁻¹ * exp (-((x - μ) / β)).
• prod_cdf_gumbelMeasure: max-stability. The product of the cdfs with locations u j and a common scale β is the cdf with location β * log (∑ j, exp (u j / β)).

noncomputable def ProbabilityTheory.gumbelPDFReal (μ : ℝ) (β : NNReal) (x : ℝ) : ℝ

The pdf of the Gumbel distribution with location μ and scale β.

Equations

• ProbabilityTheory.gumbelPDFReal μ β x = (↑β)⁻¹ * Real.exp (-((x - μ) / ↑β)) * Real.exp (-Real.exp (-((x - μ) / ↑β)))

@[simp]

theorem ProbabilityTheory.gumbelPDFReal_zero_scale (μ : ℝ) : gumbelPDFReal μ 0 = 0

theorem ProbabilityTheory.gumbelPDFReal_nonneg (μ : ℝ) (β : NNReal) (x : ℝ) : 0 ≤ gumbelPDFReal μ β x

theorem ProbabilityTheory.continuous_gumbelPDFReal (μ : ℝ) (β : NNReal) : Continuous (gumbelPDFReal μ β)

theorem ProbabilityTheory.measurable_gumbelPDFReal (μ : ℝ) (β : NNReal) : Measurable (gumbelPDFReal μ β)

theorem ProbabilityTheory.integrable_gumbelPDFReal (μ : ℝ) (β : NNReal) : MeasureTheory.Integrable (gumbelPDFReal μ β) MeasureTheory.volume

theorem ProbabilityTheory.integral_gumbelPDFReal_eq_one {β : NNReal} (μ : ℝ) (hβ : β ≠ 0) : ∫ (x : ℝ), gumbelPDFReal μ β x = 1

The pdf of the Gumbel distribution integrates to 1.

noncomputable def ProbabilityTheory.gumbelPDF (μ : ℝ) (β : NNReal) (x : ℝ) : ENNReal

The pdf of the Gumbel distribution, as a function valued in ℝ≥0∞.

Equations

• ProbabilityTheory.gumbelPDF μ β x = ENNReal.ofReal (ProbabilityTheory.gumbelPDFReal μ β x)

theorem ProbabilityTheory.measurable_gumbelPDF (μ : ℝ) (β : NNReal) : Measurable (gumbelPDF μ β)

@[simp]

theorem ProbabilityTheory.lintegral_gumbelPDF_eq_one {β : NNReal} (μ : ℝ) (hβ : β ≠ 0) : ∫⁻ (x : ℝ), gumbelPDF μ β x = 1

The pdf of the Gumbel distribution integrates to 1.

noncomputable def ProbabilityTheory.gumbelMeasure (μ : ℝ) (β : NNReal) : MeasureTheory.Measure ℝ

The Gumbel distribution on ℝ with location μ and scale β.

Equations

• ProbabilityTheory.gumbelMeasure μ β = if β = 0 then MeasureTheory.Measure.dirac μ else MeasureTheory.volume.withDensity (ProbabilityTheory.gumbelPDF μ β)

theorem ProbabilityTheory.gumbelMeasure_of_scale_ne_zero {β : NNReal} (μ : ℝ) (hβ : β ≠ 0) : gumbelMeasure μ β = MeasureTheory.volume.withDensity (gumbelPDF μ β)

@[simp]

theorem ProbabilityTheory.gumbelMeasure_zero_scale (μ : ℝ) : gumbelMeasure μ 0 = MeasureTheory.Measure.dirac μ

instance ProbabilityTheory.instIsProbabilityMeasureRealGumbelMeasure (μ : ℝ) (β : NNReal) : MeasureTheory.IsProbabilityMeasure (gumbelMeasure μ β)

theorem ProbabilityTheory.nullSingletonClass_gumbelMeasure {β : NNReal} (μ : ℝ) (hβ : β ≠ 0) : MeasureTheory.NullSingletonClass (gumbelMeasure μ β)

theorem ProbabilityTheory.cdf_gumbelMeasure_eq {β : NNReal} (μ : ℝ) (hβ : β ≠ 0) (x : ℝ) : ↑(cdf (gumbelMeasure μ β)) x = Real.exp (-Real.exp (-((x - μ) / ↑β)))

The cdf of the Gumbel distribution is exp (-exp (-((x - μ) / β))).

theorem ProbabilityTheory.gumbelPDFReal_eq_mul_cdf {β : NNReal} (μ : ℝ) (hβ : β ≠ 0) (x : ℝ) : gumbelPDFReal μ β x = (↑β)⁻¹ * Real.exp (-((x - μ) / ↑β)) * ↑(cdf (gumbelMeasure μ β)) x

The pdf of the Gumbel distribution is its cdf times the reverse hazard rate β⁻¹ * exp (-((x - μ) / β)).

theorem ProbabilityTheory.prod_cdf_gumbelMeasure {β : NNReal} {ι : Type u_1} {s : Finset ι} (hs : s.Nonempty) (u : ι → ℝ) (hβ : β ≠ 0) (x : ℝ) : ∏ j ∈ s, ↑(cdf (gumbelMeasure (u j) β)) x = ↑(cdf (gumbelMeasure (↑β * Real.log (∑ j ∈ s, Real.exp (u j / ↑β))) β)) x

Max-stability of the Gumbel family. The product of the cdfs of Gumbel distributions with locations u j and a common scale β is the cdf of the Gumbel distribution with location β * log (∑ j ∈ s, exp (u j / β)) and scale β.