Gumbel-Luce Equivalence (McFadden's Theorem) @cite{mcfadden-1974}

The exact algebraic connection between Gumbel noise in a Random Utility Model (RUM) and the Luce choice rule (softmax). @cite{luce-1959}

Random Utility Models

A Random Utility Model (RUM) assigns each alternative i a random utility:

`Uᵢ = uᵢ + εᵢ`

where uᵢ is a deterministic component and εᵢ is random noise. The choice probability is P(i chosen) = P(Uᵢ = max_j Uⱼ).

Two noise distributions yield closed-form choice probabilities:

• Gaussian noise → Φ (Thurstone Case V, §2.D of @cite{luce-1959})
• Gumbel noise → softmax (@cite{mcfadden-1974})

McFadden's Theorem

If the εᵢ are i.i.d. Gumbel(0, β), then:

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

This is exact — no approximation involved. The proof reduces to the Laplace integral ∫₀^∞ exp(-S·t) dt = 1/S after a change of variables.

Thurstone–Luce Bridge

Combined with the Thurstone result (Thurstone.lean), this gives the precise relationship between the two models:

• Gaussian noise → normal CDF (Thurstone, exact)
• Gumbel noise → logistic/softmax (Luce, exact by McFadden)
• Φ ≈ logistic (numerical approximation, max error ~0.01)

The two models are both RUMs, differing only in noise distribution. The logistic approximation to the normal CDF (Thurstone.lean §4) is what connects them, not a foundational assumption.

Main Results

• integral_exp_neg_mul_Ioi_zero: Laplace integral ∫₀^∞ exp(-S·t) dt = 1/S
• mcfaddenIntegral_eq_softmax: McFadden's theorem (algebraic core)
• mcfaddenIntegral_binary: Binary case reduces to logistic function
• gumbelCDF, gumbelPDF: Gumbel distribution definitions

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.

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.

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

The McFadden integral for alternative i with scale β > 0:

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 : ι → ℝ) {β : ℝ} (_hβ : 0 < β) (i : ι) : mcfaddenIntegral u β i = softmax u (1 / β) i

McFadden's Theorem (algebraic core) — Lemma 1 of @cite{mcfadden-1974}: The McFadden integral equals softmax.

For any utilities u₁, ..., uₙ and scale β > 0:

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

where S = Σⱼ exp(uⱼ/β).

This is the algebraic content of McFadden's Lemma 1 (p. 111), generalized from unit scale (β = 1) to arbitrary β > 0. McFadden assumes i.i.d. Weibull (Gnedenko extreme value) noise with CDF P(ε ≤ ε) = exp(-e^{-ε}) — eq. (13) — and derives the softmax selection probability P_i = e^{V_i} / Σ e^{V_j} — eq. (12). The probabilistic interpretation is formalized separately in gumbelMaxProb_is_mcfaddenIntegral.

theorem Core.mcfaddenIntegral_sum {ι : Type u_1} [Fintype ι] [Nonempty ι] (u : ι → ℝ) {β : ℝ} (hβ : 0 < β) : ∑ 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 : ι → ℝ) {β : ℝ} (hβ : 0 < β) (i : ι) : 0 < mcfaddenIntegral u β i

Each McFadden integral is positive.

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

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

mcfaddenIntegral([u₁, u₂], β)(0) = logistic((u₁ - u₂) / β)

This is the exact Gumbel-Luce result for binary choice: if ε₁, ε₂ are i.i.d. Gumbel(0, β), then P(u₁+ε₁ > u₂+ε₂) = logistic((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 → ℝ) {β : ℝ} (hβ : 0 < β) : mcfaddenIntegral u β 1 = 1 - logistic ((u 0 - u 1) / β)

The binary McFadden integral for alternative 1 is the complement.

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 : ι → ℝ) {β : ℝ} (hβ : 0 < β) (i : ι) : (fromGumbelRUM u β).policy () i = mcfaddenIntegral u β i

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

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 @cite{mcfadden-1974} (p. 111).

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

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

McFadden's proof (p. 111) with Vᵢ = v(s, xᵢ):

1. From eq. (13), F_i(ε + V_i - V_1, ..., ε + V_i - V_J) = exp(-ε) · ∏ⱼ exp(-exp(-ε - V_i + V_j)) = exp(-ε) · exp(-exp(-ε) · Σⱼ exp(V_j - V_i))
2. Substituting in eq. (3) and integrating yields eq. (12): P_i = e^{V_i} / Σⱼ e^{V_j}

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

McFadden's Lemma 2 (Uniqueness) @cite{mcfadden-1974}

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 is: if the max-CDF G satisfies the functional equation

`G(x - c) = G(x) ^ exp(c)` for all `x, c ∈ ℝ`

then G must be a Gumbel CDF: G(t) = exp(-α · exp(-t)) where α = -log(G(0)) > 0.

The proof sets x = 0 and c = -t in the functional equation, giving G(t) = G(0)^{exp(-t)}, then rewrites G(0)^y = exp(log(G(0)) · y) using 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.

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)).