Random utility models

In a random utility model the alternatives j : ι have real-valued utilities with a joint law μ on ι → ℝ, and the alternative with the highest utility is chosen. The choice probability of i is the mass μ gives to the event that coordinate i is the strict maximum. Most models take the utilities independent, μ = Measure.pi ν; noise on parameters shared by the alternatives correlates them, and such a law is a pushforward (choiceProb_map). The additive model, with utility u j + ε j for a systematic part u j and noise ε j, is the case where ν is a location family.

For independent utilities the theory is independent of the noise family. Splitting coordinate i off the product measure (measurePreserving_piSplitAt) writes the choice probability as the integral against ν i of the product of the other coordinates' distribution functions. For atomless noise ties are null, so the choice probabilities of the alternatives sum to one. Independent Gumbel noise gives the softmax rule. This direction is due to Marschak and, in constructive form, to Holman and Marley as reported by Luce and Suppes; McFadden proves it as his Lemma 1, and his Lemma 2 is the converse for choice sets of size at least three, since Yellott shows that binary logistic choice does not pin down Gumbel noise. Gaussian noise gives the probit rule, whose binary case is computed here from the convolution of two Gaussians.

Main definitions

• ProbabilityTheory.choiceProb: the probability that alternative i has the highest utility under a joint law of the utilities.

Main results

• ProbabilityTheory.choiceProb_map: the choice probabilities of a pushforward law.
• ProbabilityTheory.choiceProb_pi_eq_lintegral: for independent utilities, the choice probability as an integral against ν i.
• ProbabilityTheory.sum_choiceProb: when ties are null the choice probabilities sum to one.
• ProbabilityTheory.choiceProb_pi_gumbelMeasure: under independent Gumbel utilities the choice probabilities are softmax.
• ProbabilityTheory.choiceProb_pi_gaussianReal: two alternatives with independent Gaussian utilities of common variance v have choice probability Φ ((u 0 - u 1) / √(2 * v)).

References

• L. L. Thurstone, A law of comparative judgment (1927)
• D. McFadden, Conditional logit analysis of qualitative choice behavior (1974)
• [Mar60]
• [LS65]
• [Luc59]
• [Yel77]

Choice probabilities

noncomputable def ProbabilityTheory.choiceProb {ι : Type u_1} (μ : MeasureTheory.Measure (ι → ℝ)) (i : ι) : ENNReal

The choice probability of alternative i in the random utility model whose utilities have the joint law μ is the probability that coordinate i is the strict maximum.

Equations

• ProbabilityTheory.choiceProb μ i = μ {x : ι → ℝ | ∀ (j : ι), j ≠ i → x j < x i}

theorem ProbabilityTheory.measurableSet_setOf_forall_ne_lt {ι : Type u_1} [Fintype ι] (i : ι) : MeasurableSet {x : ι → ℝ | ∀ (j : ι), j ≠ i → x j < x i}

theorem ProbabilityTheory.choiceProb_map {ι : Type u_1} [Fintype ι] {Ω : Type u_2} [MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) {U : Ω → ι → ℝ} (hU : Measurable U) (i : ι) : choiceProb (MeasureTheory.Measure.map U P) i = P {ω : Ω | ∀ (j : ι), j ≠ i → U ω j < U ω i}

The choice probabilities of a pushforward law are the masses of the preimage events.

theorem ProbabilityTheory.sum_choiceProb {ι : Type u_1} [Fintype ι] [Nonempty ι] (μ : MeasureTheory.Measure (ι → ℝ)) [MeasureTheory.IsProbabilityMeasure μ] (hμ : ∀ (j k : ι), j ≠ k → μ {x : ι → ℝ | x j = x k} = 0) : ∑ i : ι, choiceProb μ i = 1

When ties have probability zero the choice probabilities of the alternatives sum to one, as for independent atomless noise (Measure.pi_setOf_apply_eq_apply).

theorem ProbabilityTheory.choiceProb_pi_eq_lintegral {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ν : ι → MeasureTheory.Measure ℝ) [∀ (j : ι), MeasureTheory.SigmaFinite (ν j)] (i : ι) : choiceProb (MeasureTheory.Measure.pi ν) i = ∫⁻ (x : ℝ), ∏ j ∈ Finset.univ.erase i, (ν j) (Set.Iio x) ∂ν i

The choice probability of i is the integral, against the law of the i-th utility, of the probability that every other utility falls below it.

theorem ProbabilityTheory.choiceProb_pi_eq_lintegral_cdf {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ν : ι → MeasureTheory.Measure ℝ) [∀ (j : ι), MeasureTheory.IsProbabilityMeasure (ν j)] [∀ (j : ι), MeasureTheory.NullSingletonClass (ν j)] (i : ι) : choiceProb (MeasureTheory.Measure.pi ν) i = ∫⁻ (x : ℝ), ENNReal.ofReal (∏ j ∈ Finset.univ.erase i, ↑(cdf (ν j)) x) ∂ν i

For atomless noise the choice probability integrates the product of the other alternatives' distribution functions.

Gaussian noise: the probit rule

theorem ProbabilityTheory.choiceProb_pi_gaussianReal (u : Fin 2 → ℝ) {v : NNReal} (hv : v ≠ 0) : choiceProb (MeasureTheory.Measure.pi fun (j : Fin 2) => gaussianReal (u j) v) 0 = ENNReal.ofReal (normalCDF ((u 0 - u 1) / √(2 * ↑v)))

Two alternatives with independent Gaussian utilities of means u 0, u 1 and common variance v follow the binary probit rule, since the difference of the utilities is Gaussian with variance 2 * v.

theorem ProbabilityTheory.gaussianReal_real_Ioi_zero {σ : ℝ} (Δ : ℝ) (hσ : 0 < σ) : (gaussianReal Δ (NNReal.mk (σ ^ 2) ⋯)).real (Set.Ioi 0) = normalCDF (Δ / σ)

The binary probit choice probability Φ (Δ / σ) is the mass a Gaussian with mean Δ and standard deviation σ gives to the positive half-line.

theorem ProbabilityTheory.choiceProb_pi_gaussianReal_sq {σ : ℝ} (u : Fin 2 → ℝ) (hσ : 0 < σ) : choiceProb (MeasureTheory.Measure.pi fun (j : Fin 2) => gaussianReal (u j) (NNReal.mk (σ ^ 2) ⋯)) 0 = ENNReal.ofReal (normalCDF ((u 0 - u 1) / (σ * √2)))

Two alternatives with independent Gaussian utilities of common standard deviation σ follow the probit rule with standard deviation σ * √2, that of the difference of the two utilities.

Gumbel noise: the softmax rule

theorem ProbabilityTheory.choiceProb_pi_gumbelMeasure {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] {β : NNReal} (u : ι → ℝ) (hβ : β ≠ 0) (i : ι) : choiceProb (MeasureTheory.Measure.pi fun (j : ι) => gumbelMeasure (u j) β) i = ENNReal.ofReal (Real.softmax ((↑β)⁻¹ • u) i)

When the utilities are independent with Gumbel(uⱼ, β) laws, alternative i has the highest utility with probability softmax (β⁻¹ • u) i. The density of the i-th utility times the other utilities' cdfs is softmax (β⁻¹ • u) i times the density of the maximum utility, which is Gumbel with location β * log (∑ j, exp (u j / β)) by max-stability. McFadden states the unit-scale case; the scale of the noise is not separately identified from that of u.

Binary case: the logistic function

theorem ProbabilityTheory.choiceProb_pi_gumbelMeasure_fin_two {β : NNReal} (u : Fin 2 → ℝ) (hβ : β ≠ 0) : choiceProb (MeasureTheory.Measure.pi fun (j : Fin 2) => gumbelMeasure (u j) β) 0 = ENNReal.ofReal ((u 0 - u 1) / ↑β).sigmoid

For two alternatives with Gumbel noise the choice probability is the logistic function sigmoid ((u 0 - u 1) / β). The binary probit choiceProb_pi_gaussianReal is its Gaussian counterpart, and the two are indistinguishable on binary data alone.