Binary Gaussian random utility model (probit choice)

The closed-form binary choice probability of a Gaussian random utility model: when two alternatives' utilities differ by Δ and the difference of their i.i.d. Gaussian perturbations has standard deviation σ, the probability of choosing the first is Φ(Δ / σ), where Φ is the standard normal CDF (Core.normalCDF). Equivalently it is P(X > 0) for X ~ N(Δ, σ²).

This is the probit choice rule — the Gaussian sibling of the logit (softmax) choice rule that arises from Gumbel noise (mcfaddenIntegral_binary). It is the shared, domain-neutral core that [Thu27]'s Case V model of discriminal processes (Core.ThurstoneCaseV, psychophysics) and Noisy Harmonic Grammar ([BP16], phonology) both instantiate: neither depends on the other; each applies this one fact about the normal CDF.

[UPSTREAM]: Mathlib has the Gaussian measure (gaussianReal) and a generic CDF (ProbabilityTheory.cdf), but no standard-normal CDF Φ (supplied by Core.normalCDF), no error function, and no random-utility / choice layer (this file). The grounding chain gaussianChoiceProb → normalCDF → cdf (gaussianReal 0 1) bottoms out in Mathlib's measure-theoretic Gaussian.

Main results

• gaussianChoiceProb — the probit choice probability Φ(Δ / σ).
• gaussianChoiceProb_complement — P(Δ) + P(-Δ) = 1.
• gaussianChoiceProb_strictMono — strictly increasing in the utility gap (for σ > 0).

noncomputable def Core.gaussianChoiceProb (Δ σ : ℝ) : ℝ

Binary choice probability of a Gaussian random utility model: Φ(Δ / σ), where Δ is the utility gap between the two alternatives and σ is the standard deviation of the Gaussian noise on their difference. Equivalently P(X > 0) for X ~ N(Δ, σ²) — the probit choice rule.

Equations

• Core.gaussianChoiceProb Δ σ = Core.normalCDF (Δ / σ)

@[simp]

theorem Core.gaussianChoiceProb_zero (σ : ℝ) : gaussianChoiceProb 0 σ = 1 / 2

theorem Core.gaussianChoiceProb_pos (Δ σ : ℝ) : 0 < gaussianChoiceProb Δ σ

The probit choice probability is strictly positive.

theorem Core.gaussianChoiceProb_lt_one (Δ σ : ℝ) : gaussianChoiceProb Δ σ < 1

The probit choice probability is strictly less than one.

theorem Core.gaussianChoiceProb_complement (Δ σ : ℝ) : gaussianChoiceProb Δ σ + gaussianChoiceProb (-Δ) σ = 1

Complementarity: choosing the first alternative or the second is certain.

theorem Core.half_lt_gaussianChoiceProb {Δ σ : ℝ} (hΔ : 0 < Δ) (hσ : 0 < σ) : 1 / 2 < gaussianChoiceProb Δ σ

A positive utility gap is chosen more often than chance (for σ > 0).

theorem Core.gaussianChoiceProb_lt_half {Δ σ : ℝ} (hΔ : Δ < 0) (hσ : 0 < σ) : gaussianChoiceProb Δ σ < 1 / 2

A negative utility gap is chosen less often than chance (for σ > 0).

theorem Core.gaussianChoiceProb_strictMono {σ : ℝ} (hσ : 0 < σ) : StrictMono fun (Δ : ℝ) => gaussianChoiceProb Δ σ

The choice probability is strictly increasing in the utility gap (for σ > 0).