Equation (9) — the binary odds satisfy
ProvedMcFadden1974.IIA.odds_transitivityconditional-logitdiscrete-choiceluce-choice-axiomp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1
Assume the standing conditions and Axioms 1 and 2, and write for , . For any three (not necessarily distinct) members of a possible alternative set ,
The binary odds factor through any third alternative ; this is the condition that allows a single benchmark alternative to generate all the odds.
Preamble
import Mathlib import Definitions.Def_McFadden1974_IIA_ChoiceModel
Formal statement
namespace McFadden1974.IIA
/-- **Equation (9)** (p. 110, PDF p. 6): "Permuting the indices x, y, z in Equation (6) and
multiplying yields the condition
(9) p_yx / p_xy = (p_yz/p_zy) / (p_xz/p_zx)."
Formalization Note: as in (6), `x, y, z` are members of one possible alternative set `B`, on
which the standing assumptions and Axioms 1 and 2 hold; they need not be distinct (with
`p_xx = ½` the identity holds on the diagonal too). This is the form footnote 3 applies with
`B ∪ {z}` in place of `B`. -/
theorem odds_transitivity {X S : Type*} [DecidableEq X]
(P : S → Finset X → X → ℝ) (poss : Set (Finset X))
(hprob : IsSelectionProb P poss) (hpairs : PairsPossible poss)
(hA1 : Axiom1 P poss) (hA2 : Axiom2 P poss)
(s : S) (B : Finset X) (hB : B ∈ poss) (x y z : X) (hx : x ∈ B) (hy : y ∈ B) (hz : z ∈ B) :
binProb P s y x / binProb P s x y =
(binProb P s y z / binProb P s z y) / (binProb P s x z / binProb P s z x) := by sorry
end McFadden1974.IIA
Source
McFadden, Conditional Logit Analysis of Qualitative Choice Behavior, in P. Zarembka (ed.), Frontiers in Econometrics, Academic Press (1974), p. 110, Equation (9) (PDF p. 6)
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.