Gumbel–Luce equivalence (McFadden's theorem) [McF74]

The exact algebraic connection between Gumbel noise in a random utility model (RUM) and the Luce choice rule (softmax) [Luc59].

A RUM assigns each alternative i a random utility Uᵢ = uᵢ + εᵢ, with uᵢ deterministic and εᵢ random noise, and predicts P(i chosen) = P(Uᵢ = maxⱼ Uⱼ). When the εᵢ are i.i.d. Gumbel(0, β), this probability is exactly softmax:

`P(i chosen) = exp(uᵢ/β) / Σⱼ exp(uⱼ/β) = softmax((1/β) • u)ᵢ`.

The proof reduces to the Laplace integral ∫₀^∞ exp(-S·t) dt = 1/S after the change of variables t = exp(-x/β). The Gaussian-noise counterpart (Thurstone Case V, the normal CDF) is in Thurstone.lean.

Main results

• integral_exp_neg_mul_Ioi_zero — the Laplace integral ∫₀^∞ exp(-S·t) dt = 1/S.
• mcfaddenIntegral_eq_softmax — McFadden's theorem (algebraic core).
• gumbelMaxProb_is_mcfaddenIntegral — the measure-theoretic content: the Gumbel max-probability integral equals mcfaddenIntegral.
• mcfaddenIntegral_binary — the binary case is the logistic function.
• gumbel_from_functional_eq — uniqueness: the Gumbel CDF is the only max-CDF satisfying the defining functional equation.

The Gumbel distribution

noncomputable def Core.gumbelCDF (β x : ℝ) : ℝ

The Gumbel CDF with location 0 and scale β:

F(x; β) = exp(-exp(-x/β))

The Type I extreme value distribution. Used as the noise distribution in the Luce/McFadden random utility model.

Equations

• Core.gumbelCDF β x = Real.exp (-Real.exp (-x / β))

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

The Gumbel PDF with location 0 and scale β:

f(x; β) = (1/β) · exp(-x/β) · exp(-exp(-x/β))

Equations

• Core.gumbelPDF β x = 1 / β * Real.exp (-x / β) * Real.exp (-Real.exp (-x / β))

theorem Core.gumbelCDF_pos (β x : ℝ) : 0 < gumbelCDF β x

The Gumbel CDF is strictly positive.

theorem Core.gumbelCDF_le_one (β x : ℝ) : gumbelCDF β x ≤ 1

The Gumbel CDF is at most 1.

theorem Core.gumbelPDF_pos {β : ℝ} (hβ : 0 < β) (x : ℝ) : 0 < gumbelPDF β x

The Gumbel PDF is positive when β > 0.

The Laplace integral ∫₀^∞ exp(-S·t) dt = 1/S

theorem Core.integral_exp_neg_mul_Ioi_zero {S : ℝ} (hS : 0 < S) : ∫ (t : ℝ) in Set.Ioi 0, Real.exp (-S * t) = 1 / S

The Laplace integral: ∫₀^∞ exp(-S·t) dt = 1/S for S > 0.

This is the core computation in McFadden's theorem. After the change of variables t = exp(-x/β) in the Gumbel max-probability integral, the problem reduces to this exponential integral.

Follows directly from Mathlib's integral_exp_mul_Ioi with a = -S and c = 0.

McFadden's theorem: the algebraic core

noncomputable def Core.mcfaddenIntegral {ι : Type u_1} [Fintype ι] (u : ι → ℝ) (β : ℝ) (i : ι) : ℝ

The McFadden integral for alternative i with scale β:

Iᵢ = exp(uᵢ/β) · ∫₀^∞ exp(-S·t) dt

where S = Σⱼ exp(uⱼ/β) is the partition function.

After the change of variables t = exp(-x/β) in the original Gumbel density integral, the max-probability P(Uᵢ = max_j Uⱼ) takes this form. See gumbelMaxProb_is_mcfaddenIntegral.

Equations

• Core.mcfaddenIntegral u β i = Real.exp (u i / β) * ∫ (t : ℝ) in Set.Ioi 0, Real.exp ((-∑ j : ι, Real.exp (u j / β)) * t)

theorem Core.mcfaddenIntegral_eq_softmax {ι : Type u_1} [Fintype ι] [Nonempty ι] (u : ι → ℝ) {β : ℝ} (i : ι) : mcfaddenIntegral u β i = softmax ((1 / β) • u) i

McFadden's theorem (algebraic core) — Lemma 1 of [McF74]: the McFadden integral equals softmax. For utilities u and scale β,

exp(uᵢ/β) · ∫₀^∞ exp(-S·t) dt = exp(uᵢ/β) / S = softmax((1/β) • u)ᵢ,

where S = Σⱼ exp(uⱼ/β). The identity is purely algebraic and holds for every β (the RUM-relevant case is β > 0). [McF74] assumes i.i.d. Weibull (Gnedenko extreme-value) noise with CDF exp(-e^{-ε}) and derives the softmax selection probability Pᵢ = e^{Vᵢ} / Σ e^{Vⱼ}; the probabilistic interpretation is formalized in gumbelMaxProb_is_mcfaddenIntegral.

theorem Core.mcfaddenIntegral_sum {ι : Type u_1} [Fintype ι] [Nonempty ι] (u : ι → ℝ) {β : ℝ} : ∑ i : ι, mcfaddenIntegral u β i = 1

The McFadden integrals sum to 1 (they form a probability distribution).

theorem Core.mcfaddenIntegral_pos {ι : Type u_1} [Fintype ι] [Nonempty ι] (u : ι → ℝ) {β : ℝ} (i : ι) : 0 < mcfaddenIntegral u β i

Each McFadden integral is positive.

Binary case: McFadden equals the logistic function

theorem Core.mcfaddenIntegral_binary (u : Fin 2 → ℝ) {β : ℝ} : mcfaddenIntegral u β 0 = ((u 0 - u 1) / β).sigmoid

Binary McFadden = logistic: for two alternatives, the McFadden integral reduces to the logistic function.

mcfaddenIntegral([u₁, u₂], β)(0) = Real.sigmoid((u₁ - u₂) / β)

This is the exact Gumbel-Luce result for binary choice: if ε₁, ε₂ are i.i.d. Gumbel(0, β), then P(u₁+ε₁ > u₂+ε₂) = Real.sigmoid((u₁-u₂)/β).

Compare with Thurstone Case V (Thurstone.lean): P(u₁+η₁ > u₂+η₂) = Φ((u₁-u₂)/(σ√2)) for Gaussian noise η.

theorem Core.mcfaddenIntegral_binary_one (u : Fin 2 → ℝ) {β : ℝ} : mcfaddenIntegral u β 1 = 1 - ((u 0 - u 1) / β).sigmoid

The binary McFadden integral for alternative 1 is the complement.

The Gumbel RUM as a RationalAction

noncomputable def Core.RationalAction.fromGumbelRUM {ι : Type u_1} [Fintype ι] (u : ι → ℝ) (β : ℝ) : RationalAction Unit ι

Construct a RationalAction from a Gumbel RUM.

The score function is exp(uᵢ/β), which gives Luce's choice rule. This is the exact optimal policy under i.i.d. Gumbel noise (by McFadden's theorem), not an approximation.

Equations

• Core.RationalAction.fromGumbelRUM u β = { score := fun (x : Unit) (i : ι) => Real.exp (u i / β), score_nonneg := ⋯ }

theorem Core.RationalAction.fromGumbelRUM_policy {ι : Type u_1} [Fintype ι] [Nonempty ι] (u : ι → ℝ) {β : ℝ} (i : ι) : (fromGumbelRUM u β).policy () i = mcfaddenIntegral u β i

The Gumbel RUM policy equals the McFadden integral (= softmax).

Measure-theoretic content: the Gumbel max-probability integral

theorem Core.gumbelMaxProb_is_mcfaddenIntegral {n : ℕ} (u : Fin n → ℝ) (β : ℝ) (hβ : 0 < β) (i : Fin n) : ∫ (x : ℝ), gumbelPDF β (x - u i) * ∏ j ∈ Finset.univ.erase i, gumbelCDF β (x - u j) = mcfaddenIntegral u β i

Gumbel RUM = McFadden integral — the measure-theoretic content of Lemma 1 in [McF74].

If ε₁, …, εₙ are i.i.d. Gumbel(0, β), then the probability that alternative i attains the maximum random utility equals the McFadden integral:

P(uᵢ + εᵢ = maxⱼ(uⱼ + εⱼ)) = mcfaddenIntegral u β i

The proof uses the antiderivative G(x) = (C/S) · exp(-S · exp(-x/β)) with C = exp(uᵢ/β) and S = Σⱼ exp(uⱼ/β): by the FTC on ℝ (integral_of_hasDerivAt_of_tendsto), ∫ G' = C/S = mcfaddenIntegral.

Uniqueness: Gumbel is the only distribution yielding softmax

McFadden's Lemma 2 shows that the Gumbel distribution is the only i.i.d. noise distribution yielding the softmax (Luce) choice rule. The key step: if the max-CDF G satisfies the functional equation G(x - c) = G(x) ^ exp c for all x, c, then G is a Gumbel CDF G(t) = exp(-α · exp(-t)) with α = -log(G 0) > 0. Setting x = 0, c = -t gives G t = G 0 ^ exp(-t), then G 0 ^ y = exp(log(G 0) · y) via rpow_def_of_pos.

theorem Core.gumbel_from_functional_eq (G : ℝ → ℝ) (hG0_pos : 0 < G 0) (_hG0_lt : G 0 < 1) (hfe : ∀ (x c : ℝ), G (x - c) = G x ^ Real.exp c) (t : ℝ) : G t = Real.exp (- -Real.log (G 0) * Real.exp (-t))

If a function G satisfies the functional equation G(x - c) = G(x) ^ exp(c) for all x, c ∈ ℝ, and 0 < G(0) < 1, then G is a Gumbel CDF:

G(t) = exp(-α · exp(-t)) where α = -log(G(0)) > 0.

This is the core of McFadden's Lemma 2: the functional equation characterizing the max-CDF uniquely determines the Gumbel family. The hypothesis G 0 < 1 is unused in this proof but pins down α > 0 (see gumbel_alpha_pos), excluding the degenerate α = 0 case.

theorem Core.gumbel_alpha_pos (G : ℝ → ℝ) (hG0_pos : 0 < G 0) (hG0_lt : G 0 < 1) : 0 < -Real.log (G 0)

The scale parameter α = -log(G(0)) is positive when 0 < G(0) < 1.

theorem Core.gumbel_standard_from_functional_eq (G : ℝ → ℝ) (hG0 : G 0 = Real.exp (-1)) (hfe : ∀ (x c : ℝ), G (x - c) = G x ^ Real.exp c) (t : ℝ) : G t = Real.exp (-Real.exp (-t))

When G(0) = e⁻¹ (i.e., α = 1), the functional equation gives the standard Gumbel CDF: G(t) = exp(-exp(-t)).