Gumbel–Luce equivalence [McF74]

A random utility model assigns each alternative i the utility uᵢ + εᵢ and chooses the maximizer; with i.i.d. Gumbel noise the choice probabilities are exactly softmax, P(i) = exp(uᵢ/β) / ∑ⱼ exp(uⱼ/β). The Gumbel→softmax direction is due to [Mar60] and, in the constructive form given here, to Holman and Marley (via [LS65]); [McF74] proves it as his Lemma 1 and credits them. McFadden's own contribution is the converse, Lemma 2: among translation-complete i.i.d. noise distributions only the Gumbel family yields the Luce rule [Luc59]. Uniqueness genuinely needs choice sets of size ≥ 3: for binary choice the logistic form does not pin down Gumbel noise (Yellott [Yel77]; compare the binary probit in Core/Probability/RandomUtility.lean).

The distribution layer (density, measure, CDF, max-stability, and the max-probability integral) lives in Core/Probability/Gumbel.lean; this file gives it the random-utility reading.

Main definitions

• RationalAction.fromGumbelRUM: the Luce agent of a Gumbel RUM, defined as fromSoftmax at inverse temperature β⁻¹.

Main results

• rumMaxProb_gumbel_eq_softmax: Lemma 1 of [McF74] — the Gumbel max-probability integral is softmax.
• rumMaxProb_gumbel_binary: the binary case is the logistic function.
• gumbel_from_functional_eq, eq_cdf_gumbelMeasure_of_functional_eq: the terminal step of Lemma 2 — a noise CDF satisfying G(x-c) = G(x)^{exp c} is Gumbel. McFadden derives that equation only for positive-integer exp c (duplicated alternatives) and extends by monotonicity; the derivation of the equation from the softmax form and translation completeness is not formalized here.

theorem Core.rumMaxProb_gumbel_eq_softmax {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] {β : ℝ} (u : ι → ℝ) (hβ : 0 < β) (i : ι) : rumMaxProb (gumbelPDFReal 0 β) (fun (x : ℝ) => ↑(ProbabilityTheory.cdf (gumbelMeasure 0 β)) x) u i = softmax ((1 / β) • u) i

Gumbel RUM ⟹ softmax (Lemma 1 of [McF74], due to Holman and Marley via Luce and Suppes): the max-probability integral of utilities u under i.i.d. Gumbel(0, β) noise equals softmax ((1/β) • u).

[McF74] states the unit-scale case; the β-generalization is standard (the scale of the noise is not separately identified from the scale of u).

theorem Core.rumMaxProb_gumbel_sum {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] {β : ℝ} (u : ι → ℝ) (hβ : 0 < β) : ∑ i : ι, rumMaxProb (gumbelPDFReal 0 β) (fun (x : ℝ) => ↑(ProbabilityTheory.cdf (gumbelMeasure 0 β)) x) u i = 1

The Gumbel RUM policy sums to 1 over alternatives — inherited from softmax_sum_eq_one through rumMaxProb_gumbel_eq_softmax.

Binary case: the logistic function

theorem Core.rumMaxProb_gumbel_binary (u : Fin 2 → ℝ) {β : ℝ} (hβ : 0 < β) : rumMaxProb (gumbelPDFReal 0 β) (fun (x : ℝ) => ↑(ProbabilityTheory.cdf (gumbelMeasure 0 β)) x) u 0 = ((u 0 - u 1) / β).sigmoid

Binary Gumbel RUM = logistic: for two alternatives the choice probability is sigmoid ((u 0 - u 1) / β). Compare Thurstone Case V (Processing/Psychophysics/Thurstone.lean): Φ((u 0 - u 1)/(σ√2)) for Gaussian noise. By [Yel77] the two are indistinguishable on binary data alone.

The Gumbel RUM as a RationalAction

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

The Luce agent of a Gumbel RUM: score exp(uᵢ/β). This is fromSoftmax at inverse temperature β⁻¹ — exact under i.i.d. Gumbel(0, β) noise by Lemma 1 of [McF74], not an approximation.

Equations

• Core.RationalAction.fromGumbelRUM u β = Core.RationalAction.fromSoftmax (fun (x : Unit) => u) β⁻¹

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

The Gumbel RUM policy is softmax at inverse temperature β⁻¹.

Uniqueness: the terminal step of McFadden's Lemma 2

Lemma 2 of [McF74] assumes softmax selection probabilities on every finite subset of a universe, representative utilities ranging over all of ℝ, and i.i.d. noise with a translation complete CDF G; it concludes G is Gumbel. Playing duplicated alternatives off against each other yields G(x - log K) = G(x)^K for positive integers K, which extends to the real functional equation by monotonicity. The theorems below formalize the terminal step only: solving the (real-strength) functional equation.

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

A noise CDF satisfying G(x - c) = G(x) ^ exp c with 0 < G 0 has the Gumbel form G(t) = exp (log (G 0) · exp (-t)).

theorem Core.eq_cdf_gumbelMeasure_of_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 = ↑(ProbabilityTheory.cdf (gumbelMeasure (Real.log (-Real.log (G 0))) 1)) t

With the nondegeneracy bound G 0 < 1, the functional equation pins G to an honest Gumbel CDF: G = cdf (gumbelMeasure (log (-log (G 0))) 1).