Rank Orderings @cite{luce-1959}

@cite{luce-1959}: the probability of observing a complete rank ordering under the Luce choice rule. The key insight is that ranking probability decomposes into a product of successive top-choices from shrinking alternative sets — a direct consequence of IIA.

Main results

• rankProb: probability of a ranking (as a List) under the Luce model, defined as the product of successive pChoice values from shrinking tails.
• rankProb_eq_score_prod: express ranking probability in terms of score ratios v(aᵢ) / ∑ⱼ≥ᵢ v(aⱼ) (Theorem 9).
• rankProb_sum_eq_one: ranking probabilities over all permutations sum to 1.
• rankProb_marginal_first: marginalizing rankings over the first choice recovers pChoice.

def Core.tailSuffix {A : Type u_2} [DecidableEq A] (ranking : List A) (i : ℕ) : Finset A

The tail suffix of a list starting at position i (0-indexed). Used to represent the shrinking alternative set at each step of ranking.

Equations

• Core.tailSuffix ranking i = (List.drop i ranking).toFinset

noncomputable def Core.rankStepProb {S : Type u_1} {A : Type u_2} [Fintype A] [DecidableEq A] (ra : RationalAction S A) (s : S) (ranking : List A) (i : ℕ) : ℝ

Probability of a single step in the ranking: choosing ranking[i] from the remaining alternatives {ranking[i], ranking[i+1],...}.

Equations

• Core.rankStepProb ra s ranking i = match ranking[i]? with | none => 1 | some a => ra.pChoice s (Core.tailSuffix ranking i) a

noncomputable def Core.rankProb {S : Type u_1} {A : Type u_2} [Fintype A] [DecidableEq A] (ra : RationalAction S A) (s : S) (ranking : List A) : ℝ

Ranking probability (@cite{luce-1959}, Theorem 9): The probability of observing the complete rank ordering a₁ > a₂ >... > aₙ is the product of successive top-choices from shrinking sets:

P(a₁ > a₂ >... > aₙ) = P(a₁ | {a₁,...,aₙ}) · P(a₂ | {a₂,...,aₙ}) ·... · P(aₙ₋₁ | {aₙ₋₁, aₙ})

Under the Luce model with ratio scale v, this becomes: P(a₁ >... > aₙ) = ∏ᵢ v(aᵢ) / ∑ⱼ≥ᵢ v(aⱼ)

Equations

• Core.rankProb ra s ranking = List.foldl (fun (acc : ℝ) (i : ℕ) => acc * Core.rankStepProb ra s ranking i) 1 (List.range ranking.length)

noncomputable def Core.rankProbRec {S : Type u_1} {A : Type u_2} [Fintype A] [DecidableEq A] (ra : RationalAction S A) (s : S) : List A → ℝ

Recursive characterization of ranking probability: the first-choice probability times the ranking probability of the remaining alternatives.

Equations

• Core.rankProbRec ra s [] = 1
• Core.rankProbRec ra s (a :: rest) = ra.pChoice s (a :: rest).toFinset a * Core.rankProbRec ra s rest

theorem Core.rankProbRec_eq_rankProb {S : Type u_1} {A : Type u_2} [Fintype A] [DecidableEq A] (ra : RationalAction S A) (s : S) (ranking : List A) : rankProbRec ra s ranking = rankProb ra s ranking

rankProbRec agrees with the explicit rankProb definition.

Proof by list induction. The key steps use:

• List.range_succ_eq_map to decompose range(n+1) = 0 :: map succ (range n)
• List.foldl_map to shift indices through the map
• foldl_mul_comm_init to factor out the first-choice probability
• Definitional equalities: rankStepProb (a::rest) 0 = pChoice and rankStepProb (a::rest) (i+1) = rankStepProb rest i

theorem Core.rankProb_nonneg {S : Type u_1} {A : Type u_2} [Fintype A] [DecidableEq A] (ra : RationalAction S A) (s : S) (ranking : List A) : 0 ≤ rankProb ra s ranking

Ranking probability is non-negative: each factor is a pChoice value, hence non-negative.

noncomputable def Core.scoreRatio {S : Type u_1} {A : Type u_2} [Fintype A] [DecidableEq A] (ra : RationalAction S A) (s : S) (ranking : List A) (i : ℕ) : ℝ

The score-ratio factor at position i: v(aᵢ) / ∑ⱼ≥ᵢ v(aⱼ). This is the i-th factor in the score-product form of ranking probability.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Core.rankProbScoreProd {S : Type u_1} {A : Type u_2} [Fintype A] [DecidableEq A] (ra : RationalAction S A) (s : S) (ranking : List A) : ℝ

The score-product form of ranking probability: ∏ᵢ v(aᵢ) / ∑ⱼ≥ᵢ v(aⱼ).

Equations

• Core.rankProbScoreProd ra s ranking = List.foldl (fun (acc : ℝ) (i : ℕ) => acc * Core.scoreRatio ra s ranking i) 1 (List.range ranking.length)

theorem Core.rankProb_eq_score_prod {S : Type u_1} {A : Type u_2} [Fintype A] [DecidableEq A] (ra : RationalAction S A) (s : S) (ranking : List A) (_hnd : ranking.Nodup) : rankProb ra s ranking = rankProbScoreProd ra s ranking

Theorem 9 (score form): ranking probability equals the product of score ratios.

Each pChoice factor equals the corresponding score ratio by definition of the Luce choice rule, so the two products are term-by-term equal.

noncomputable def Core.allRankings {A : Type u_2} [DecidableEq A] (T : Finset A) : Finset (List A)

All permutations of a finset, as lists.

Equations

• Core.allRankings T = T.val.toList.permutations.toFinset

theorem Core.mem_allRankings_iff {A : Type u_2} [DecidableEq A] (T : Finset A) (ranking : List A) : ranking ∈ allRankings T ↔ ranking.toFinset = T ∧ ranking.Nodup

Every ranking in allRankings T is a permutation of T.

Uses List.mem_permutations, List.perm_ext_iff_of_nodup, and Multiset.mem_toList from mathlib to connect the List-level permutation API with Finset membership.

theorem Core.rankProb_sum_eq_one {S : Type u_1} {A : Type u_2} [Fintype A] [DecidableEq A] (ra : RationalAction S A) (s : S) (T : Finset A) (hT : T.Nonempty) (hpos : ∀ a ∈ T, 0 < ra.score s a) : ∑ r ∈ allRankings T, rankProb ra s r = 1

Ranking probabilities sum to 1 (@cite{luce-1959}, Theorem 9 completeness): Over all n! permutations of the alternative set, ranking probabilities form a proper distribution.

The proof proceeds by induction on |T|:

• Base (T = ∅): allRankings ∅ = {[]}, rankProb [] = 1.
• Step: decompose allRankings T by first element, factor out pChoice (which sums to 1 by pChoice_sum_eq_one), and apply the inductive hypothesis to each (n-1)-element ranking.

Requires strictly positive scores (Luce's ratio scale assumption).

noncomputable def Core.rankingsStartingWith {A : Type u_2} [DecidableEq A] (T : Finset A) (a : A) : Finset (List A)

Rankings starting with a given element a.

Equations

• Core.rankingsStartingWith T a = {r ∈ Core.allRankings T | r.head? = some a}

theorem Core.rankProb_marginal_first {S : Type u_1} {A : Type u_2} [Fintype A] [DecidableEq A] (ra : RationalAction S A) (s : S) (T : Finset A) (a : A) (ha : a ∈ T) (hpos : ∀ b ∈ T, 0 < ra.score s b) : ∑ r ∈ rankingsStartingWith T a, rankProb ra s r = ra.pChoice s T a

Marginal first-choice (@cite{luce-1959}, Theorem 9 corollary): Summing the ranking probability over all rankings that start with a recovers the choice probability pChoice(a, T).

This is because P(a first) = P(a | T) · ∑_σ P(σ | T \ {a}) = P(a | T) · 1, where the inner sum equals 1 by rankProb_sum_eq_one on the remaining alternatives.

def Core.rankOf {A : Type u_2} [DecidableEq A] (ranking : List A) (a : A) : ℕ

The rank of element a in a ranking (1-indexed, so rank 1 = best). Returns 0 if a is not in the ranking.

Equations

• Core.rankOf ranking a = if a ∈ ranking then List.findIdx (fun (x : A) => x == a) ranking + 1 else 0

noncomputable def Core.expectedRank {S : Type u_1} {A : Type u_2} [Fintype A] [DecidableEq A] (ra : RationalAction S A) (s : S) (T : Finset A) (a : A) : ℝ

Expected rank of alternative a under the ranking distribution.

E[rank(a)] = ∑_σ P(σ) · rank(a, σ)

The monotonicity theorem expectedRank_lt_of_score_gt shows that alternatives with higher v(a) have lower (better) expected rank.

Equations

• Core.expectedRank ra s T a = ∑ r ∈ Core.allRankings T, Core.rankProb ra s r * ↑(Core.rankOf r a)

theorem Core.expectedRank_lt_of_score_gt {S : Type u_1} {A : Type u_2} [Fintype A] [DecidableEq A] (ra : RationalAction S A) (s : S) (T : Finset A) (a₁ a₂ : A) (ha₁ : a₁ ∈ T) (ha₂ : a₂ ∈ T) (hne : a₁ ≠ a₂) (hpos : ∀ a ∈ T, 0 < ra.score s a) (hgt : ra.score s a₁ > ra.score s a₂) : expectedRank ra s T a₁ < expectedRank ra s T a₂

Expected rank monotonicity: higher score implies lower expected rank.

If v(a₁) > v(a₂) then E[rank(a₁)] < E[rank(a₂)]: the alternative with higher ratio-scale value is expected to be ranked higher (closer to 1).

This is a natural property of the Plackett–Luce model (@cite{luce-1959}, @cite{plackett-1975}) but does not appear as a formal theorem in either source. @cite{luce-1959} proves ranking probability decomposition (Theorem 9) and @cite{marden-1995} covers estimation, but neither states the expected rank monotonicity result explicitly.

The proof uses conditional expectation decomposition: E[rank(a, T)] = 1 + ∑_{b≠a} pChoice(b,T) · E[rank(a, T\{b})] and combines within-set induction with cross-set monotonicity (a higher-scored element gets better expected rank against the same field).

theorem Core.expectedRank_eq_of_score_eq {S : Type u_1} {A : Type u_2} [Fintype A] [DecidableEq A] (ra : RationalAction S A) (s : S) (T : Finset A) (a₁ a₂ : A) (ha₁ : a₁ ∈ T) (ha₂ : a₂ ∈ T) (hne : a₁ ≠ a₂) (hpos : ∀ a ∈ T, 0 < ra.score s a) (heq : ra.score s a₁ = ra.score s a₂) : expectedRank ra s T a₁ = expectedRank ra s T a₂

Equal scores imply equal expected ranks: if score(a₁) = score(a₂), then E[rank(a₁, T)] = E[rank(a₂, T)].

The proof uses the conditional expectation decomposition and antisymmetry: decompose both expected ranks by first element, show the common terms are equal by induction, and show the cross terms are equal by applying expectedRank_cross_le_aux in both directions (since v(a₁) ≥ v(a₂) and v(a₂) ≥ v(a₁) both hold).