Gumbel distribution

The Gumbel (Type I extreme value) distribution over ℝ, in the register of Mathlib.Probability.Distributions.*: density → measure via withDensity → CDF as a theorem. Application-agnostic — the random-utility reading lives in Core/Probability/Choice/GumbelLuce.lean.

Main definitions

• gumbelPDFReal: the density β⁻¹ · exp(-(x-μ)/β) · exp(-exp(-(x-μ)/β)) with location μ and scale β.
• gumbelPDF: the ℝ≥0∞-valued density.
• gumbelMeasure: the Gumbel measure, volume.withDensity (gumbelPDF μ β).

Main results

• cdf_gumbelMeasure_eq: the CDF is exp(-exp(-(x-μ)/β)).
• prod_cdf_gumbelMeasure: max-stability — the product of Gumbel CDFs with common scale is the Gumbel CDF at location β * log (∑ exp (uⱼ/β)).
• integral_gumbelPDFReal_mul_prod_cdf: the max-probability integral of a Gumbel random-utility family evaluates to exp(uᵢ/β) / ∑ⱼ exp(uⱼ/β).

Mathlib upstream candidates

Mathlib has no Gumbel (or any extreme-value) distribution (verified 2026-08-01 against Mathlib.Probability.Distributions.*); this whole file follows the Pareto.lean template and is an upstream candidate. integrableOn_gumbelPDFReal_Iic inlines a reflection argument because mathlib has integrableOn_Ioi_deriv_of_nonneg' but no Iic mirror — that general lemma is a separate small upstream candidate.

Density

noncomputable def Core.gumbelPDFReal (μ β x : ℝ) : ℝ

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

Equations

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

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

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

Equations

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

theorem Core.measurable_gumbelPDFReal (μ β : ℝ) : Measurable (gumbelPDFReal μ β)

theorem Core.stronglyMeasurable_gumbelPDFReal (μ β : ℝ) : MeasureTheory.StronglyMeasurable (gumbelPDFReal μ β)

theorem Core.gumbelPDFReal_pos {β : ℝ} (hβ : 0 < β) (μ x : ℝ) : 0 < gumbelPDFReal μ β x

theorem Core.gumbelPDFReal_nonneg {β : ℝ} (hβ : 0 ≤ β) (μ x : ℝ) : 0 ≤ gumbelPDFReal μ β x

theorem Core.hasDerivAt_gumbelCDF (μ β x : ℝ) : HasDerivAt (fun (y : ℝ) => Real.exp (-Real.exp (-((y - μ) / β)))) (gumbelPDFReal μ β x) x

The Gumbel cdf exp (-exp (-(x - μ)/β)) is an antiderivative of the pdf.

theorem Core.tendsto_gumbelCDF_atTop {β : ℝ} (hβ : 0 < β) (μ : ℝ) : Filter.Tendsto (fun (y : ℝ) => Real.exp (-Real.exp (-((y - μ) / β)))) Filter.atTop (nhds 1)

theorem Core.tendsto_gumbelCDF_atBot {β : ℝ} (hβ : 0 < β) (μ : ℝ) : Filter.Tendsto (fun (y : ℝ) => Real.exp (-Real.exp (-((y - μ) / β)))) Filter.atBot (nhds 0)

theorem Core.integrableOn_gumbelPDFReal_Ioi {β : ℝ} (hβ : 0 < β) (μ a : ℝ) : MeasureTheory.IntegrableOn (gumbelPDFReal μ β) (Set.Ioi a) MeasureTheory.volume

theorem Core.integrableOn_gumbelPDFReal_Iic {β : ℝ} (hβ : 0 < β) (μ a : ℝ) : MeasureTheory.IntegrableOn (gumbelPDFReal μ β) (Set.Iic a) MeasureTheory.volume

theorem Core.integrable_gumbelPDFReal {β : ℝ} (hβ : 0 < β) (μ : ℝ) : MeasureTheory.Integrable (gumbelPDFReal μ β) MeasureTheory.volume

theorem Core.integral_gumbelPDFReal_eq_one {β : ℝ} (hβ : 0 < β) (μ : ℝ) : ∫ (x : ℝ), gumbelPDFReal μ β x = 1

The pdf of the Gumbel distribution integrates to 1.

@[simp]

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

Measure and CDF

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

Measure defined by the Gumbel distribution.

Equations

• Core.gumbelMeasure μ β = MeasureTheory.volume.withDensity (Core.gumbelPDF μ β)

theorem Core.isProbabilityMeasure_gumbelMeasure {β : ℝ} (hβ : 0 < β) (μ : ℝ) : MeasureTheory.IsProbabilityMeasure (gumbelMeasure μ β)

theorem Core.cdf_gumbelMeasure_eq_integral {β : ℝ} (hβ : 0 < β) (μ x : ℝ) : ↑(ProbabilityTheory.cdf (gumbelMeasure μ β)) x = ∫ (y : ℝ) in Set.Iic x, gumbelPDFReal μ β y

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

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

Max-stability and the max-probability integral

theorem Core.prod_cdf_gumbelMeasure {β : ℝ} {ι : Type u_1} [Fintype ι] [Nonempty ι] (u : ι → ℝ) (hβ : 0 < β) (x : ℝ) : ∏ j : ι, ↑(ProbabilityTheory.cdf (gumbelMeasure (u j) β)) x = ↑(ProbabilityTheory.cdf (gumbelMeasure (β * Real.log (∑ j : ι, Real.exp (u j / β))) β)) x

Max-stability of the Gumbel family: the product of independent Gumbel CDFs with common scale β is Gumbel with scale β and location β * log (∑ exp (uⱼ/β)).

theorem Core.integral_gumbelPDFReal_mul_prod_cdf {β : ℝ} {ι : Type u_1} [Fintype ι] [Nonempty ι] [DecidableEq ι] (u : ι → ℝ) (hβ : 0 < β) (i : ι) : ∫ (x : ℝ), gumbelPDFReal (u i) β x * ∏ j ∈ Finset.univ.erase i, ↑(ProbabilityTheory.cdf (gumbelMeasure (u j) β)) x = Real.exp (u i / β) / ∑ j : ι, Real.exp (u j / β)

The max-probability integral of a Gumbel random-utility family: the density formula for the event that alternative i attains the maximum evaluates to exp(uᵢ/β) / ∑ⱼ exp(uⱼ/β).