Equation (42) — logit selection probabilities are bounded below by $1/(J_* e^{2M|\theta|})$

Proved

McFadden1974.Asymptotics.prob_lower_bound

by mikedeng1 · Oct 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

asymptotic-statisticsconditional-logitmaximum-likelihoodp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Suppose every observation $m$ has at most $J_*$ alternatives and every vector of independent variables satisfies $|z_{im}| \le M$ (the boundedness part of Axiom 7). Then for every observation $m$ , alternative $i$ and parameter $\theta \in \mathbb R^K$ the conditional logit selection probability satisfies

P_{im}(\theta) \ \ge\ \frac{1}{J_*\, e^{2M|\theta|}} \;=\; P_* > 0 .

The bound is uniform in the observation, so on bounded sets of parameters every alternative has probability bounded away from zero. It drives the probability estimate in the proof of Lemma 5.

Formalization Note The printed $1/J_*e^{2M|\theta|}$ is read as $1/(J_* e^{2M|\theta|})$ . Norms are Euclidean.

Preamble

import Mathlib
import Definitions.Def_McFadden1974_Asymptotics_LogitSample

Formal statement

namespace McFadden1974.Asymptotics

open MeasureTheory ProbabilityTheory Filter Topology

/-- **Equation (42)** (Lemma 5, proof, p. 135, PDF p. 31): "The selection probabilities are
bounded below by (42) P_in ≥ 1/J_* e^{2M|θ|} ≡ P_* > 0, where J_* and M are the bounds given by
Axiom 7."

Formalization Note: the printed `1/J_* e^{2M|θ|}` is read as `1/(J_* e^{2M|θ|})`. Only the
boundedness part of Axiom 7 is assumed (`IsBounded`), with Euclidean norms on `z` and `θ`.
`J_* ≥ J_m ≥ 1`, so the bound is a positive real number; the bound holds for every observation,
alternative and parameter. -/
theorem prob_lower_bound {K : ℕ} (D : SerialData K) (Jstar : ℕ) (M : ℝ)
    (hB : IsBounded D Jstar M) (m : ℕ) (i : Fin (D.J m)) (θ : EuclideanSpace ℝ (Fin K)) :
    1 / ((Jstar : ℝ) * Real.exp (2 * M * ‖θ‖)) ≤ prob D m i θ := by sorry

end McFadden1974.Asymptotics

Source

McFadden, Conditional Logit Analysis of Qualitative Choice Behavior, in P. Zarembka (ed.), Frontiers in Econometrics, Academic Press (1974), p. 135, Equation (42) (Lemma 5, proof); PDF p. 31

Human review

Endorsed by Shuze Chen · Oct 5, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 5, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Equation (42) — logit selection probabilities are bounded below by 1/(J∗e2M∣θ∣)1/(J_* e^{2M|\theta|})1/(J∗​e2M∣θ∣)

Equation (42) — logit selection probabilities are bounded below by $1/(J_* e^{2M|\theta|})$