Rank orderings under the Luce choice rule

This file defines the probability of a complete rank ordering as the product of successive top-choices from shrinking alternative sets — the ranking postulate of [Luc59] (§2.F, p. 72), now known as the Plackett–Luce model ([Pla75]). We show that these probabilities sum to 1 over all permutations, that marginalizing over the first choice recovers pChoice, and that adjacent transpositions (rankProb_swap_div) and expected rank (expectedRank_lt_of_score_gt) both respect the score order.

Main definitions

• rankProb: probability of a ranking (as a List) under the Luce rule.
• expectedRank: expected (1-indexed) rank of an alternative.

References

• R. D. Luce, Individual Choice Behavior
• R. L. Plackett, The Analysis of Permutations

Ranking probability ([Luc59], §2.F, pp. 68–74)

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 ([Luc59]'s ranking postulate, p. 72): 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.

theorem Core.rankProbRec_pos {S : Type u_1} {A : Type u_2} [Fintype A] [DecidableEq A] (ra : RationalAction S A) (s : S) (ranking : List A) (hpos : ∀ (b : A), 0 < ra.score s b) : 0 < rankProbRec ra s ranking

rankProbRec is positive when all scores are positive.

theorem Core.rankProb_pos {S : Type u_1} {A : Type u_2} [Fintype A] [DecidableEq A] (ra : RationalAction S A) (s : S) (ranking : List A) (hpos : ∀ (b : A), 0 < ra.score s b) : 0 < rankProb ra s ranking

Ranking probability is positive when all scores are positive.

Score-ratio form

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

Score form: ranking probability equals the product of score ratios.

Summation over permutations

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.

Decomposition of allRankings by first element

Ranking probabilities sum to 1

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: over all n! permutations of the alternative set, ranking probabilities form a proper distribution. Requires strictly positive scores (Luce's ratio scale assumption).

Marginalization: recovering pChoice

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: summing the ranking probability over all rankings that start with a recovers the choice probability pChoice(a, T). ([Luc59]'s own Theorem 9, p. 72, is the pairwise analogue: P(x,y) is recovered by summing over rankings placing x above y.)

Adjacent transpositions

theorem Core.rankProbRec_cons {S : Type u_1} {A : Type u_2} [Fintype A] [DecidableEq A] (ra : RationalAction S A) (s : S) {a : A} {l : List A} (ha : a ∉ l) (hpos : ∀ (b : A), 0 < ra.score s b) : rankProbRec ra s (a :: l) = ra.score s a / (ra.score s a + ∑ b ∈ l.toFinset, ra.score s b) * rankProbRec ra s l

One step of rankProbRec in score form, for a head not repeated in the tail.

theorem Core.rankProb_swap_div {S : Type u_1} {A : Type u_2} [Fintype A] [DecidableEq A] (ra : RationalAction S A) (s : S) (x y : A) (rest : List A) (hx : x ∉ rest) (hy : y ∉ rest) (hpos : ∀ (b : A), 0 < ra.score s b) : rankProb ra s (x :: y :: rest) / rankProb ra s (y :: x :: rest) = (ra.score s x + ∑ b ∈ rest.toFinset, ra.score s b) / (ra.score s y + ∑ b ∈ rest.toFinset, ra.score s b)

Swapping two adjacent elements scales the ranking probability by (v x + S) / (v y + S), where S sums the scores of the remaining alternatives — not by the naive v x / v y: the second step of each ranking draws from a different set.

theorem Core.rankProb_swap_lt_of_score_lt {S : Type u_1} {A : Type u_2} [Fintype A] [DecidableEq A] (ra : RationalAction S A) (s : S) {x y : A} (rest : List A) (hx : x ∉ rest) (hy : y ∉ rest) (hpos : ∀ (b : A), 0 < ra.score s b) (hlt : ra.score s y < ra.score s x) : rankProb ra s (y :: x :: rest) < rankProb ra s (x :: y :: rest)

Swapping adjacent elements into score order strictly increases ranking probability: if v y < v x, then x before y is the more probable order.

Expected rank

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)

Expected rank monotonicity: infrastructure

Expected rank decomposition:

E[rank(a,T)] = 1 + ∑_{b≠a} pChoice(b) · E[rank(a,T\{b})]

Cross-set monotonicity

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 ([Luc59], [Pla75]) but does not appear as a formal theorem in either source. [Luc59] adopts the product decomposition as his ranking postulate and [Mar95] covers estimation, but neither states the expected rank monotonicity result explicitly.

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).