From 40a786977b393c7a6c1009aa74a302a9ab7ae3f6 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Sat, 1 Aug 2026 01:23:10 -0300 Subject: [PATCH] refactor(Core/Probability/Choice): dissolve SemiorderRanking bridge --- Linglib.lean | 1 - .../Choice/ChoiceApproximations.lean | 144 +++------ .../Probability/Choice/RankOrderings.lean | 223 +++++++------- .../Probability/Choice/RationalAction.lean | 41 ++- .../Probability/Choice/SemiorderRanking.lean | 285 ------------------ Linglib/Studies/CohnGordonEtAl2019.lean | 1 - Linglib/Studies/EgreEtAl2023.lean | 2 +- blog/references.bib | 27 ++ 8 files changed, 224 insertions(+), 500 deletions(-) delete mode 100644 Linglib/Core/Probability/Choice/SemiorderRanking.lean diff --git a/Linglib.lean b/Linglib.lean index 1fea61b99..c936b029e 100644 --- a/Linglib.lean +++ b/Linglib.lean @@ -275,7 +275,6 @@ import Linglib.Core.Probability.Choice.ChoiceApproximations import Linglib.Core.Probability.Choice.GumbelLuce import Linglib.Core.Probability.Choice.RankOrderings import Linglib.Core.Probability.Choice.RationalAction -import Linglib.Core.Probability.Choice.SemiorderRanking import Linglib.Core.Probability.ConditionalProbability import Linglib.Core.Probability.Confirmation import Linglib.Core.Probability.Constructions diff --git a/Linglib/Core/Probability/Choice/ChoiceApproximations.lean b/Linglib/Core/Probability/Choice/ChoiceApproximations.lean index 8fcc8f708..bcb4c85da 100644 --- a/Linglib/Core/Probability/Choice/ChoiceApproximations.lean +++ b/Linglib/Core/Probability/Choice/ChoiceApproximations.lean @@ -1,51 +1,35 @@ import Linglib.Core.Probability.Choice.RationalAction /-! -# Algebraic Approximations ([luce-1959], §1.G, pp. 34–37) [luce-1959] +# Just noticeable differences and the trace -[luce-1959] develops the connection between choice probabilities and -ordinal preference structures via **just noticeable differences** (jnds). +This file formalizes the algebraic approximations of [luce-1959] (§1.G, +pp. 34–37). A jnd threshold `π ∈ (1/2, 1)` splits pairwise choice into a +discriminable-preference relation `L(π)` and an indistinguishability relation +`I(π)` (Definition 3). We show that the pair satisfies Luce's semiorder +axioms (Theorem 5) and that the trace ordering (Definition 4) is a weak order +coinciding with the ratio-scale order (Theorem 6). -When stimuli are "close" in value, subjects cannot reliably discriminate -between them — the choice probability `P(x, {x,y})` is near `1/2`. A jnd -threshold `π ∈ (1/2, 1)` defines two relations on the alternative set: +## Main definitions -- **L(π)**: `x` is discriminably preferred to `y` (Definition 3) -- **I(π)**: `x` and `y` are indistinguishable (Definition 3) +* `jndL`, `jndI`: the relations `L(π)` and `I(π)`. +* `traceGe`: the trace ordering `x ≥_T y`. -## Key results +## References -1. **Semiorder** (Theorem 5): Under Axiom 1 with imperfect discrimination, - `(L(π), I(π))` satisfies the semiorder axioms — trichotomy, I-reflexivity, - L-transitivity, and the interval condition `xLy ∧ yIz ∧ zLw → xLw`. - -2. **Trace** (Definition 4): `x ≥_T y` iff `P(x, z) ≥ P(y, z)` for all `z`. - The trace extracts the "underlying" preference by requiring dominance in - all pairwise comparisons against any third alternative. - -3. **Weak order** (Theorem 6): Under Axiom 1, the trace is a weak order - (total preorder), and `x ≥_T y` iff `v(x) ≥ v(y)` iff `P(x, y) ≥ 1/2`. - -## Connection to the choice axiom - -The semiorder captures the *observable* preference structure (what a subject -can discriminate), while the trace recovers the *latent* ratio scale ordering. -Theorem 6 shows that Axiom 1 forces these to align: the trace is exactly the -ordering induced by the scale values `v`. +* [R. D. Luce, *Individual Choice Behavior*][luce-1959] -/ namespace Core open Real BigOperators Finset -variable {A : Type*} [DecidableEq A] +variable {A : Type*} -- The pairwise kernel `pairwiseProb` and its lemma suite live in -- `Core.Probability.Choice.RationalAction` (imported above). --- ============================================================================ --- §2. Just Noticeable Differences (Definition 3, p. 34) --- ============================================================================ +/-! ### Just noticeable differences (Definition 3, p. 34) -/ /-- The `L(π)` relation (Definition 3, [luce-1959], p. 34): `x L(π) y` iff `P(x, {x,y}) > π`. @@ -67,12 +51,8 @@ def jndL (v : A → ℝ) (thr : ℝ) (x y : A) : Prop := def jndI (v : A → ℝ) (thr : ℝ) (x y : A) : Prop := 1 - thr ≤ pairwiseProb v x y ∧ pairwiseProb v x y ≤ thr --- ============================================================================ --- §3. Semiorder Properties (Theorem 5, p. 35) --- ============================================================================ - /-! -## Semiorder axioms +### Semiorder axioms (Theorem 5, p. 35) [luce-1959] defines a **semiordering** of a set `U` as a pair `(L, I)` of relations satisfying, for all `x, y, z, w ∈ U`: @@ -85,31 +65,25 @@ def jndI (v : A → ℝ) (thr : ℝ) (x y : A) : Prop := Theorem 5 proves these hold for `(L(π), I(π))` under Axiom 1. -/ -/-- I(π) is symmetric: if `x` and `y` are indistinguishable, so are `y` and `x`. - - Since `P(y,x) = 1 - P(x,y)`, the condition `1-π ≤ P(x,y) ≤ π` - is equivalent to `1-π ≤ P(y,x) ≤ π`. -/ +/-- I(π) is symmetric: if `x` and `y` are indistinguishable, so are `y` and + `x`. -/ theorem jndI_symm (v : A → ℝ) (hv : ∀ a : A, 0 < v a) (thr : ℝ) (x y : A) (h : jndI v thr x y) : jndI v thr y x := by simp only [jndI] at * have hc := pairwiseProb_complement (hv x) (hv y) constructor <;> linarith [h.1, h.2] -/-- **I-reflexivity**: `x I(π) x`, since `P(x, x) = 1/2` and `1-π < 1/2 < π` - whenever `1/2 < π < 1`. -/ +/-- **I-reflexivity**: `x I(π) x`. -/ theorem jndI_refl (v : A → ℝ) (hv : ∀ a : A, 0 < v a) (thr : ℝ) (hthr_lower : 1 / 2 < thr) (_hthr_upper : thr < 1) (x : A) : jndI v thr x x := by simp only [jndI, pairwiseProb_self (hv x)] constructor <;> linarith -/-- **Trichotomy**: for any `x, y`, exactly one of `xLy`, `yLx`, or `xIy` holds. - - Since `P(x,y) + P(y,x) = 1`, the three conditions `P(x,y) > π`, - `P(y,x) > π` (i.e., `P(x,y) < 1-π`), and `1-π ≤ P(x,y) ≤ π` - partition the interval `[0, 1]`. -/ +/-- **Trichotomy**: for any `x, y`, exactly one of `xLy`, `yLx`, or `xIy` + holds. -/ theorem jnd_trichotomy (v : A → ℝ) (hv : ∀ a : A, 0 < v a) (thr : ℝ) - (_hthr_lower : 1 / 2 < thr) (_hthr_upper : thr < 1) (x y : A) : + (hthr_lower : 1 / 2 < thr) (_hthr_upper : thr < 1) (x y : A) : (jndL v thr x y ∧ ¬jndL v thr y x ∧ ¬jndI v thr x y) ∨ (jndL v thr y x ∧ ¬jndL v thr x y ∧ ¬jndI v thr x y) ∨ (jndI v thr x y ∧ ¬jndL v thr x y ∧ ¬jndL v thr y x) := by @@ -123,36 +97,7 @@ theorem jnd_trichotomy (v : A → ℝ) (hv : ∀ a : A, 0 < v a) (thr : ℝ) · push Not at h₂ right; right; exact ⟨⟨by linarith, h₁⟩, fun h => by linarith, fun h => by linarith⟩ -omit [DecidableEq A] in -/-- **L-transitivity**: `xLy ∧ yLz → xLz`. - - Under Axiom 1, `P(x,y) > π` means `v(x)/(v(x)+v(y)) > π`, i.e., - `v(x)/v(y) > π/(1-π)`. If also `v(y)/v(z) > π/(1-π)`, then - `v(x)/v(z) > (π/(1-π))² > π/(1-π)` (since `π/(1-π) > 1`), - so `P(x,z) > π`. -/ -theorem jndL_trans (v : A → ℝ) (hv : ∀ a : A, 0 < v a) (thr : ℝ) - (hthr_lower : 1 / 2 < thr) (_hthr_upper : thr < 1) (x y z : A) - (hxy : jndL v thr x y) (hyz : jndL v thr y z) : - jndL v thr x z := by - simp only [jndL, pairwiseProb] at * - have hvx := hv x; have hvy := hv y; have hvz := hv z - rw [lt_div_iff₀ (add_pos hvx hvy)] at hxy - rw [lt_div_iff₀ (add_pos hvy hvz)] at hyz - rw [lt_div_iff₀ (add_pos hvx hvz)] - have h1 : thr * v y < (1 - thr) * v x := by nlinarith - have h2 : thr * v z < (1 - thr) * v y := by nlinarith - nlinarith [mul_pos (by linarith : (0:ℝ) < 1 - thr) hvy] - -omit [DecidableEq A] in -/-- **Interval condition**: `xLy ∧ yIz ∧ zLw → xLw`. - - Under Axiom 1: `xLy` gives `v(x)/v(y) > π/(1-π)`, `yIz` gives - `v(y)/v(z) ≥ (1-π)/π` (from `P(y,z) ≥ 1-π`), and `zLw` gives - `v(z)/v(w) > π/(1-π)`. Multiplying the first and third ratios and - using the bound on `v(y)/v(z)`: - `v(x)/v(w) = (v(x)/v(y)) · (v(y)/v(z)) · (v(z)/v(w)) > π/(1-π)` - since the middle factor is ≥ (1-π)/π and the outer factors are > π/(1-π), - giving a product > (π/(1-π))·((1-π)/π)·(π/(1-π)) = π/(1-π). -/ +/-- **Interval condition**: `xLy ∧ yIz ∧ zLw → xLw`. -/ theorem jndL_interval (v : A → ℝ) (hv : ∀ a : A, 0 < v a) (thr : ℝ) (_hthr_lower : 1 / 2 < thr) (_hthr_upper : thr < 1) (x y z w : A) (hxy : jndL v thr x y) (hyz : jndI v thr y z) (hzw : jndL v thr z w) : @@ -170,13 +115,8 @@ theorem jndL_interval (v : A → ℝ) (hv : ∀ a : A, 0 < v a) (thr : ℝ) -- Chain: thr * v(w) < (1-thr) * v(z) ≤ thr * v(y) < (1-thr) * v(x) linarith -omit [DecidableEq A] in -/-- **No sandwiching**: `xLy ∧ yLz → ¬(xIw ∧ wIz)`. - - If `v(x) ≫ v(y) ≫ v(z)` (both with ratio > π/(1-π)), then no - `w` can be indistinguishable from both `x` and `z`: such a `w` - would need `v(w) ≈ v(x)` and `v(w) ≈ v(z)` simultaneously, but - `v(x)/v(z) > (π/(1-π))² ≫ 1` prevents this. -/ +/-- **No sandwiching**: `xLy ∧ yLz → ¬(xIw ∧ wIz)` — no `w` can be + indistinguishable from both endpoints of a discriminable chain. -/ theorem jndL_no_sandwich (v : A → ℝ) (hv : ∀ a : A, 0 < v a) (thr : ℝ) (hthr_lower : 1 / 2 < thr) (hthr_upper : thr < 1) (x y z w : A) (hxy : jndL v thr x y) (hyz : jndL v thr y z) : @@ -206,9 +146,17 @@ theorem jndL_no_sandwich (v : A → ℝ) (hv : ∀ a : A, 0 < v a) (thr : ℝ) mul_lt_mul_of_pos_right hxy (hv z), mul_lt_mul_of_pos_right hyz (hv x)] --- ============================================================================ --- §4. The Trace (Definition 4 and Theorem 6, p. 37) --- ============================================================================ +/-- **L-transitivity**: `xLy ∧ yLz → xLz`. Not one of the semiorder axioms — + it follows from the interval condition instantiated at `z := y`, via + I-reflexivity. -/ +theorem jndL_trans (v : A → ℝ) (hv : ∀ a : A, 0 < v a) (thr : ℝ) + (hthr_lower : 1 / 2 < thr) (hthr_upper : thr < 1) (x y z : A) + (hxy : jndL v thr x y) (hyz : jndL v thr y z) : + jndL v thr x z := + jndL_interval v hv thr hthr_lower hthr_upper x y y z hxy + (jndI_refl v hv thr hthr_lower hthr_upper y) hyz + +/-! ### The trace (Definition 4 and Theorem 6, p. 37) -/ /-- The trace relation (Definition 4, [luce-1959], p. 37): `x ≥_T y` iff `P(x, z) ≥ P(y, z)` for all `z`. @@ -220,15 +168,8 @@ theorem jndL_no_sandwich (v : A → ℝ) (hv : ∀ a : A, 0 < v a) (thr : ℝ) def traceGe (v : A → ℝ) (x y : A) : Prop := ∀ z : A, pairwiseProb v y z ≤ pairwiseProb v x z -/-- **Theorem 6**: Under Axiom 1, the trace relation - is equivalent to `v(x) ≥ v(y)`. - - **Proof sketch**: Under Axiom 1, `P(x,z) = v(x)/(v(x)+v(z))`. Since - `t ↦ t/(t+c)` is monotone increasing for `c > 0`, we have - `P(x,z) ≥ P(y,z)` for all `z` iff `v(x) ≥ v(y)`. - - (→) Take `z = y`: `P(x,y) ≥ P(y,y) = 1/2`, hence `v(x) ≥ v(y)`. - (←) If `v(x) ≥ v(y)`, monotonicity of `t/(t+c)` gives `P(x,z) ≥ P(y,z)`. -/ +/-- **Theorem 6**: the trace relation is equivalent to the scale ordering + `v(y) ≤ v(x)`. -/ theorem trace_iff_scale_ge (v : A → ℝ) (hv : ∀ a : A, 0 < v a) (x y : A) : traceGe v x y ↔ v y ≤ v x := by simp only [traceGe] @@ -246,7 +187,6 @@ theorem trace_iff_pairwiseProb_ge_half (v : A → ℝ) (hv : ∀ a : A, 0 < v a) traceGe v x y ↔ 1 / 2 ≤ pairwiseProb v x y := by rw [trace_iff_scale_ge v hv, pairwiseProb_ge_half_iff (hv x) (hv y)] -omit [DecidableEq A] in /-- The trace is reflexive: `x ≥_T x`. -/ theorem traceGe_refl (v : A → ℝ) (x : A) : traceGe v x x := λ _ => le_refl _ @@ -259,18 +199,14 @@ theorem traceGe_trans (v : A → ℝ) (hv : ∀ a : A, 0 < v a) (x y z : A) linarith /-- The trace is total: for any `x, y`, either `x ≥_T y` or `y ≥_T x`. - - This completes the proof that the trace is a **weak order** (total - preorder). Under Axiom 1, the trace is determined by the ratio scale - values, which are totally ordered reals. -/ + With `traceGe_refl` and `traceGe_trans`, the trace is a **weak order** + (total preorder). -/ theorem traceGe_total (v : A → ℝ) (hv : ∀ a : A, 0 < v a) (x y : A) : traceGe v x y ∨ traceGe v y x := by rw [trace_iff_scale_ge v hv, trace_iff_scale_ge v hv] exact le_total (v y) (v x) -/-- The trace agrees with L: if `xLy` for any `π`, then `x ≥_T y`. - - `P(x,y) > π > 1/2` implies `v(x) > v(y)` implies `x ≥_T y`. -/ +/-- The trace agrees with L: if `xLy` for any `π`, then `x ≥_T y`. -/ theorem traceGe_of_jndL (v : A → ℝ) (hv : ∀ a : A, 0 < v a) (thr : ℝ) (hthr : 1 / 2 < thr) (x y : A) (h : jndL v thr x y) : traceGe v x y := by diff --git a/Linglib/Core/Probability/Choice/RankOrderings.lean b/Linglib/Core/Probability/Choice/RankOrderings.lean index 48a9e79cf..1ece8d2a3 100644 --- a/Linglib/Core/Probability/Choice/RankOrderings.lean +++ b/Linglib/Core/Probability/Choice/RankOrderings.lean @@ -1,23 +1,25 @@ import Linglib.Core.Probability.Choice.RationalAction /-! -# Rank Orderings [luce-1959] +# Rank orderings under the Luce choice rule -[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. +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 [luce-1959] (§2.F, p. 72), now known as the Plackett–Luce model +([plackett-1975]). 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 results +## Main definitions -- `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`. +* `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*][luce-1959] +* [R. L. Plackett, *The Analysis of Permutations*][plackett-1975] -/ namespace Core @@ -26,9 +28,7 @@ open BigOperators Finset Real variable {S A : Type*} [Fintype A] [DecidableEq A] --- ============================================================================ --- §2.F Rank Orderings ([luce-1959], pp. 66–72) --- ============================================================================ +/-! ### Ranking probability ([luce-1959], §2.F, pp. 68–74) -/ /-- The tail suffix of a list starting at position `i` (0-indexed). Used to represent the shrinking alternative set at each step of ranking. -/ @@ -43,7 +43,7 @@ noncomputable def rankStepProb (ra : RationalAction S A) (s : S) | none => 1 | some a => ra.pChoice s (tailSuffix ranking i) a -/-- **Ranking probability** ([luce-1959], Theorem 9): +/-- **Ranking probability** ([luce-1959]'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: @@ -126,9 +126,22 @@ theorem rankProb_nonneg (ra : RationalAction S A) (s : S) (ranking : List A) : 0 ≤ rankProb ra s ranking := foldl_mul_nonneg one_pos.le (rankStepProb_nonneg ra s ranking) _ --- ============================================================================ --- Score-ratio form (Theorem 9, second part) --- ============================================================================ +/-- `rankProbRec` is positive when all scores are positive. -/ +theorem rankProbRec_pos (ra : RationalAction S A) (s : S) (ranking : List A) + (hpos : ∀ b, 0 < ra.score s b) : 0 < rankProbRec ra s ranking := by + induction ranking with + | nil => simp [rankProbRec] + | cons a rest ih => + show 0 < ra.pChoice s (a :: rest).toFinset a * rankProbRec ra s rest + exact mul_pos + (RationalAction.pChoice_pos (by simp [List.toFinset_cons]) fun b _ => hpos b) ih + +/-- Ranking probability is positive when all scores are positive. -/ +theorem rankProb_pos (ra : RationalAction S A) (s : S) (ranking : List A) + (hpos : ∀ b, 0 < ra.score s b) : 0 < rankProb ra s ranking := + rankProbRec_eq_rankProb ra s ranking ▸ rankProbRec_pos ra s ranking hpos + +/-! ### Score-ratio form -/ /-- 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. -/ @@ -155,7 +168,7 @@ private theorem mem_tailSuffix_of_getElem? a ∈ tailSuffix ranking i := by simp only [tailSuffix, List.mem_toFinset] have hi : i < ranking.length := by - by_contra hc; push_neg at hc + by_contra hc; push Not at hc simp [List.getElem?_eq_none hc] at h rw [List.drop_eq_getElem_cons hi] have hval : ranking[i] = a := by @@ -176,10 +189,7 @@ private theorem rankStepProb_eq_scoreRatio (ra : RationalAction S A) (s : S) have hmem : a ∈ tailSuffix ranking i := mem_tailSuffix_of_getElem? h simp only [RationalAction.pChoice, hmem, ↓reduceIte] -/-- **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. -/ +/-- **Score form**: ranking probability equals the product of score ratios. -/ theorem rankProb_eq_score_prod (ra : RationalAction S A) (s : S) (ranking : List A) (_hnd : ranking.Nodup) : rankProb ra s ranking = rankProbScoreProd ra s ranking := by @@ -188,9 +198,7 @@ theorem rankProb_eq_score_prod (ra : RationalAction S A) (s : S) (ranking : List ext acc i exact congrArg (acc * ·) (rankStepProb_eq_scoreRatio ra s ranking i) --- ============================================================================ --- Summation over permutations (Theorem 9, completeness) --- ============================================================================ +/-! ### Summation over permutations -/ /-- All permutations of a finset, as lists. -/ noncomputable def allRankings (T : Finset A) : Finset (List A) := @@ -220,9 +228,7 @@ theorem mem_allRankings_iff (T : Finset A) (ranking : List A) : rw [← List.mem_toFinset (l := ranking), hfs, Multiset.mem_toList, Finset.mem_val] --- ============================================================================ --- Decomposition of allRankings by first element --- ============================================================================ +/-! ### Decomposition of `allRankings` by first element -/ /-- Cons into allRankings: if `rest ∈ allRankings (T.erase a)` and `a ∈ T`, then `a :: rest ∈ allRankings T`. -/ @@ -309,9 +315,7 @@ private theorem rankProb_cons_eq (ra : RationalAction S A) (s : S) ra.pChoice s T a * rankProbRec ra s rest rw [hfs] --- ============================================================================ --- Theorem 9 completeness: ranking probabilities sum to 1 --- ============================================================================ +/-! ### Ranking probabilities sum to 1 -/ /-- Score positivity propagates to erased subsets. -/ private theorem score_pos_erase {ra : RationalAction S A} {s : S} @@ -362,16 +366,8 @@ private theorem rankProb_sum_eq_one_aux (ra : RationalAction S A) (s : S) : rw [Finset.sum_congr rfl step] exact ra.pChoice_sum_eq_one s T (score_sum_ne_zero hT hpos) -/-- **Ranking probabilities sum to 1** ([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. - +/-- **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). -/ theorem rankProb_sum_eq_one (ra : RationalAction S A) (s : S) (T : Finset A) (hT : T.Nonempty) @@ -379,9 +375,7 @@ theorem rankProb_sum_eq_one (ra : RationalAction S A) (s : S) ∑ r ∈ allRankings T, rankProb ra s r = 1 := rankProb_sum_eq_one_aux ra s T.card T rfl hpos --- ============================================================================ --- Marginalization (recovering pChoice) --- ============================================================================ +/-! ### Marginalization: recovering `pChoice` -/ /-- Rankings starting with a given element `a`. -/ noncomputable def rankingsStartingWith (T : Finset A) (a : A) : Finset (List A) := @@ -404,13 +398,11 @@ private theorem rankingsStartingWith_eq (T : Finset A) (a : A) (ha : a ∈ T) : · rintro ⟨rest, hrest, rfl⟩ exact ⟨cons_mem_allRankings ha hrest, by simp⟩ -/-- **Marginal first-choice** ([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. -/ +/-- **Marginal first-choice**: summing the ranking probability over all + rankings that start with `a` recovers the choice probability + `pChoice(a, T)`. ([luce-1959]'s own Theorem 9, p. 72, is the pairwise + analogue: `P(x,y)` is recovered by summing over rankings placing `x` + above `y`.) -/ theorem rankProb_marginal_first (ra : RationalAction S A) (s : S) (T : Finset A) (a : A) (ha : a ∈ T) (hpos : ∀ b ∈ T, 0 < ra.score s b) : @@ -434,9 +426,70 @@ theorem rankProb_marginal_first (ra : RationalAction S A) (s : S) Finset.insert_empty, Finset.sum_singleton, rankProb] simp [mul_one] --- ============================================================================ --- Expected rank monotonicity --- ============================================================================ +/-! ### Adjacent transpositions -/ + +/-- One step of `rankProbRec` in score form, for a head not repeated in the + tail. -/ +theorem rankProbRec_cons (ra : RationalAction S A) (s : S) {a : A} {l : List A} + (ha : a ∉ l) (hpos : ∀ b, 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 := by + have hnot : a ∉ l.toFinset := by rwa [List.mem_toFinset] + have hsum : ra.score s a + ∑ b ∈ l.toFinset, ra.score s b ≠ 0 := + (add_pos_of_pos_of_nonneg (hpos a) (Finset.sum_nonneg fun b _ => (hpos b).le)).ne' + show ra.pChoice s (a :: l).toFinset a * rankProbRec ra s l = _ + rw [List.toFinset_cons, + ra.pChoice_eq_div s _ a (Finset.mem_insert_self a l.toFinset) + (by rwa [Finset.sum_insert hnot]), + Finset.sum_insert hnot] + +/-- 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 rankProb_swap_div (ra : RationalAction S A) (s : S) (x y : A) + (rest : List A) (hx : x ∉ rest) (hy : y ∉ rest) + (hpos : ∀ b, 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) := by + rw [← rankProbRec_eq_rankProb, ← rankProbRec_eq_rankProb] + have hS : 0 ≤ ∑ b ∈ rest.toFinset, ra.score s b := + Finset.sum_nonneg fun b _ => (hpos b).le + have hvx := (hpos x).ne' + have hvy := (hpos y).ne' + have htail := (rankProbRec_pos ra s rest hpos).ne' + have hxS := (add_pos_of_pos_of_nonneg (hpos x) hS).ne' + have hyS := (add_pos_of_pos_of_nonneg (hpos y) hS).ne' + have hT : (0:ℝ) < ∑ b ∈ (x :: y :: rest).toFinset, ra.score s b := + Finset.sum_pos (fun b _ => hpos b) ⟨x, by simp⟩ + have hT_eq : (y :: x :: rest).toFinset = (x :: y :: rest).toFinset := by + simp only [List.toFinset_cons] + exact Finset.insert_comm y x rest.toFinset + show ra.pChoice s (x :: y :: rest).toFinset x * rankProbRec ra s (y :: rest) / + (ra.pChoice s (y :: x :: rest).toFinset y * rankProbRec ra s (x :: rest)) = _ + rw [hT_eq, rankProbRec_cons ra s hy hpos, rankProbRec_cons ra s hx hpos, + ra.pChoice_eq_div s _ x (by simp) hT.ne', ra.pChoice_eq_div s _ y (by simp) hT.ne'] + field_simp + +/-- Swapping adjacent elements into score order strictly increases ranking + probability: if `v y < v x`, then `x` before `y` is the more probable + order. -/ +theorem rankProb_swap_lt_of_score_lt (ra : RationalAction S A) (s : S) {x y : A} + (rest : List A) (hx : x ∉ rest) (hy : y ∉ rest) + (hpos : ∀ b, 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) := by + have hden := rankProb_pos ra s (y :: x :: rest) hpos + have hS : 0 ≤ ∑ b ∈ rest.toFinset, ra.score s b := + Finset.sum_nonneg fun b _ => (hpos b).le + have h1 : 1 < rankProb ra s (x :: y :: rest) / rankProb ra s (y :: x :: rest) := by + rw [rankProb_swap_div ra s x y rest hx hy hpos, + one_lt_div (add_pos_of_pos_of_nonneg (hpos y) hS)] + linarith + exact (one_lt_div hden).mp h1 + +/-! ### Expected rank -/ /-- The rank of element `a` in a ranking (1-indexed, so rank 1 = best). Returns 0 if `a` is not in the ranking. -/ @@ -453,9 +506,7 @@ noncomputable def expectedRank (ra : RationalAction S A) (s : S) (T : Finset A) (a : A) : ℝ := ∑ r ∈ allRankings T, rankProb ra s r * (rankOf r a : ℝ) --- ============================================================================ --- Expected rank monotonicity: infrastructure --- ============================================================================ +/-! ### Expected rank monotonicity: infrastructure -/ /-- `rankOf (a :: rest) a = 1`: the first element has rank 1. -/ private theorem rankOf_cons_self (a : A) (rest : List A) : @@ -470,36 +521,8 @@ private theorem rankOf_cons_ne {b a : A} {rest : List A} simp only [rankOf, hmem, ha, ↓reduceIte, List.findIdx_cons] simp [show (b == a) = false from by simp [hne]] -/-- Positive scores imply strictly positive `pChoice`. -/ -private theorem pChoice_pos {ra : RationalAction S A} {s : S} - {T : Finset A} {a : A} (ha : a ∈ T) - (hpos : ∀ b ∈ T, 0 < ra.score s b) : - 0 < ra.pChoice s T a := by - have hsum_pos : 0 < ∑ b ∈ T, ra.score s b := - Finset.sum_pos (fun b hb => hpos b hb) ⟨a, ha⟩ - simp only [RationalAction.pChoice, ha, ne_of_gt hsum_pos, ↓reduceIte] - exact div_pos (hpos a ha) hsum_pos - -/-- Higher score implies higher `pChoice` in the same set. -/ -private theorem pChoice_gt_of_score_gt {ra : RationalAction S A} {s : S} - {T : Finset A} {a₁ a₂ : A} (ha₁ : a₁ ∈ T) (ha₂ : a₂ ∈ T) - (hpos : ∀ b ∈ T, 0 < ra.score s b) - (hgt : ra.score s a₁ > ra.score s a₂) : - ra.pChoice s T a₁ > ra.pChoice s T a₂ := by - have hratio := ra.pChoice_ratio s T a₁ a₂ ha₁ ha₂ - have hp₂ := pChoice_pos ha₂ hpos - have hv₂ := hpos a₂ ha₂ - -- From ratio: pChoice(a₁) * v(a₂) = pChoice(a₂) * v(a₁) > pChoice(a₂) * v(a₂) - have h : ra.pChoice s T a₂ * ra.score s a₂ < ra.pChoice s T a₁ * ra.score s a₂ := by - rw [show ra.pChoice s T a₁ * ra.score s a₂ = - ra.pChoice s T a₂ * ra.score s a₁ from hratio] - exact mul_lt_mul_of_pos_left hgt hp₂ - -- Divide both sides by v(a₂) > 0 - exact lt_of_mul_lt_mul_right h (le_of_lt hv₂) - --- ============================================================================ --- Expected rank decomposition: E[rank(a,T)] = 1 + ∑_{b≠a} pChoice(b) · E[rank(a,T\{b})] --- ============================================================================ +/-! ### Expected rank decomposition: +`E[rank(a,T)] = 1 + ∑_{b≠a} pChoice(b) · E[rank(a,T\{b})]` -/ /-- Inner sum when the first element equals `a`: contributes `pChoice(a, T)`. -/ private theorem expectedRank_first_self (ra : RationalAction S A) (s : S) @@ -605,9 +628,7 @@ private theorem expectedRank_ge_one (ra : RationalAction S A) (s : S) (rankProb_nonneg ra s r) _ = 1 := by simp [rankProb_sum_eq_one ra s T hT hpos] --- ============================================================================ --- Cross-set monotonicity --- ============================================================================ +/-! ### Cross-set monotonicity -/ /-- Singleton expected rank: `E[rank(a, {a})] = 1`. -/ private theorem expectedRank_singleton (ra : RationalAction S A) (s : S) (a : A) @@ -719,14 +740,9 @@ private theorem expectedRank_cross_le_aux (ra : RationalAction S A) (s : S) : This is a natural property of the Plackett–Luce model ([luce-1959], [plackett-1975]) but does not appear as a formal theorem in either - source. [luce-1959] proves ranking probability decomposition (Theorem 9) - and [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). -/ + source. [luce-1959] adopts the product decomposition as his ranking + postulate and [marden-1995] covers estimation, but neither states the + expected rank monotonicity result explicitly. -/ theorem expectedRank_lt_of_score_gt (ra : RationalAction S A) (s : S) (T : Finset A) (a₁ a₂ : A) (ha₁ : a₁ ∈ T) (ha₂ : a₂ ∈ T) (hne : a₁ ≠ a₂) @@ -769,7 +785,7 @@ theorem expectedRank_lt_of_score_gt (ra : RationalAction S A) (s : S) -- Fact 2: cross term satisfies p₂*E₁' < p₁*E₂' have h_cross : ra.pChoice s T a₂ * expectedRank ra s (T.erase a₂) a₁ < ra.pChoice s T a₁ * expectedRank ra s (T.erase a₁) a₂ := by - have hp_gt := pChoice_gt_of_score_gt ha₁' ha₂' hpos' hgt + have hp_gt := RationalAction.pChoice_lt_of_score_lt ha₁' ha₂' hpos' hgt have hE₁'_ge := expectedRank_ge_one ra s (T.erase a₂) a₁ ha₁_e₂ (score_pos_erase hpos' a₂) -- Cross-set comparison: E₁' ≤ E₂' have hE_cross : expectedRank ra s (T.erase a₂) a₁ ≤ @@ -795,7 +811,8 @@ theorem expectedRank_lt_of_score_gt (ra : RationalAction S A) (s : S) < ra.pChoice s T a₁ * expectedRank ra s (T.erase a₂) a₁ := mul_lt_mul_of_pos_right hp_gt (by linarith) _ ≤ ra.pChoice s T a₁ * expectedRank ra s (T.erase a₁) a₂ := - mul_le_mul_of_nonneg_left hE_cross (le_of_lt (pChoice_pos ha₁' hpos')) + mul_le_mul_of_nonneg_left hE_cross + (le_of_lt (RationalAction.pChoice_pos ha₁' hpos')) -- Combine: 1 + p₂*E₁' + Σ₁ < 1 + p₁*E₂' + Σ₂ linarith [Finset.sum_le_sum h_sums] diff --git a/Linglib/Core/Probability/Choice/RationalAction.lean b/Linglib/Core/Probability/Choice/RationalAction.lean index bf4c0e120..f36f50f10 100644 --- a/Linglib/Core/Probability/Choice/RationalAction.lean +++ b/Linglib/Core/Probability/Choice/RationalAction.lean @@ -321,12 +321,33 @@ theorem RationalAction.pChoice_ratio [DecidableEq A] (ra : RationalAction S A) ( · simp · next hne => field_simp -/-- Helper: `pChoice` value for `a ∈ T` with nonzero total. -/ -private theorem RationalAction.pChoice_mem [DecidableEq A] (ra : RationalAction S A) (s : S) +/-- `pChoice` in score form for `a ∈ T` with nonzero total. -/ +theorem RationalAction.pChoice_eq_div [DecidableEq A] (ra : RationalAction S A) (s : S) (T : Finset A) (a : A) (ha : a ∈ T) (hT : ∑ b ∈ T, ra.score s b ≠ 0) : ra.pChoice s T a = ra.score s a / ∑ b ∈ T, ra.score s b := by simp only [pChoice, ha, hT, ↓reduceIte] +/-- `pChoice` is positive on members when all scores in the subset are positive. -/ +theorem RationalAction.pChoice_pos [DecidableEq A] {ra : RationalAction S A} {s : S} + {T : Finset A} {a : A} (ha : a ∈ T) (hpos : ∀ b ∈ T, 0 < ra.score s b) : + 0 < ra.pChoice s T a := by + have hsum : 0 < ∑ b ∈ T, ra.score s b := Finset.sum_pos hpos ⟨a, ha⟩ + rw [ra.pChoice_eq_div s T a ha hsum.ne'] + exact div_pos (hpos a ha) hsum + +/-- Higher score implies higher `pChoice` in the same set. -/ +theorem RationalAction.pChoice_lt_of_score_lt [DecidableEq A] {ra : RationalAction S A} + {s : S} {T : Finset A} {a₁ a₂ : A} (ha₁ : a₁ ∈ T) (ha₂ : a₂ ∈ T) + (hpos : ∀ b ∈ T, 0 < ra.score s b) (hlt : ra.score s a₂ < ra.score s a₁) : + ra.pChoice s T a₂ < ra.pChoice s T a₁ := by + have hratio := ra.pChoice_ratio s T a₁ a₂ ha₁ ha₂ + have hp₂ := RationalAction.pChoice_pos ha₂ hpos + have h : ra.pChoice s T a₂ * ra.score s a₂ < ra.pChoice s T a₁ * ra.score s a₂ := by + rw [show ra.pChoice s T a₁ * ra.score s a₂ = ra.pChoice s T a₂ * ra.score s a₁ from + hratio] + exact mul_lt_mul_of_pos_left hlt hp₂ + exact lt_of_mul_lt_mul_right h (hpos a₂ ha₂).le + /-- IIA: `P(a, S) = P(a, T) / Σ_{b∈S} P(b, T)` for `S ⊆ T`. Choice probability from a subset is the conditional probability. -/ theorem RationalAction.iia [DecidableEq A] (ra : RationalAction S A) (s : S) @@ -335,11 +356,11 @@ theorem RationalAction.iia [DecidableEq A] (ra : RationalAction S A) (s : S) (hS_pos : ∑ b ∈ S', ra.score s b ≠ 0) (hT_pos : ∑ b ∈ T, ra.score s b ≠ 0) : ra.pChoice s S' a = ra.pChoice s T a / ∑ b ∈ S', ra.pChoice s T b := by - rw [ra.pChoice_mem s S' a ha hS_pos, ra.pChoice_mem s T a (hST ha) hT_pos] + rw [ra.pChoice_eq_div s S' a ha hS_pos, ra.pChoice_eq_div s T a (hST ha) hT_pos] have hsum : ∑ b ∈ S', ra.pChoice s T b = (∑ b ∈ S', ra.score s b) / ∑ c ∈ T, ra.score s c := by have : ∀ b ∈ S', ra.pChoice s T b = ra.score s b / ∑ c ∈ T, ra.score s c := - fun b hb => ra.pChoice_mem s T b (hST hb) hT_pos + fun b hb => ra.pChoice_eq_div s T b (hST hb) hT_pos rw [Finset.sum_congr rfl this, Finset.sum_div] rw [hsum] field_simp @@ -354,7 +375,7 @@ theorem RationalAction.product_rule [DecidableEq A] (ra : RationalAction S A) (s (hT_pos : ∑ b ∈ T, ra.score s b ≠ 0) : ra.pChoice s T a = ra.pChoice s S' a * ((∑ b ∈ S', ra.score s b) / ∑ b ∈ T, ra.score s b) := by - rw [ra.pChoice_mem s T a (hST ha) hT_pos, ra.pChoice_mem s S' a ha hS_pos] + rw [ra.pChoice_eq_div s T a (hST ha) hT_pos, ra.pChoice_eq_div s S' a ha hS_pos] have hS_ne : (∑ b ∈ S', ra.score s b) ≠ 0 := hS_pos rw [div_mul_div_comm, show ra.score s a * ∑ b ∈ S', ra.score s b = (∑ b ∈ S', ra.score s b) * ra.score s a from mul_comm _ _, @@ -574,6 +595,16 @@ theorem pairwiseProb_exp (u : A → ℝ) (x y : A) : end PairwiseProb +/-- Binary choice from a pair: `pChoice` on `{x, y}` is the pairwise kernel + `pairwiseProb` applied to the agent's score in that state. -/ +theorem RationalAction.pChoice_pair [DecidableEq A] (ra : RationalAction S A) (s : S) + {x y : A} (hne : x ≠ y) (hx : 0 < ra.score s x) (hy : 0 < ra.score s y) : + ra.pChoice s {x, y} x = pairwiseProb (ra.score s) x y := by + rw [ra.pChoice_eq_div s _ x (Finset.mem_insert_self x {y}) + (by rw [Finset.sum_pair hne]; exact (add_pos hx hy).ne'), + Finset.sum_pair hne] + rfl + /-! ### Alternative forms of the choice axiom [luce-1959] proves three equivalent formulations of the choice axiom: diff --git a/Linglib/Core/Probability/Choice/SemiorderRanking.lean b/Linglib/Core/Probability/Choice/SemiorderRanking.lean deleted file mode 100644 index adb73edc5..000000000 --- a/Linglib/Core/Probability/Choice/SemiorderRanking.lean +++ /dev/null @@ -1,285 +0,0 @@ -import Linglib.Core.Probability.Choice.ChoiceApproximations -import Linglib.Core.Probability.Choice.RankOrderings - -/-! -# Semiorder–Ranking Bridge [luce-1959] - -Connects the two halves of [luce-1959] that are formalized independently in -`ChoiceApproximations.lean` (§1.G) and `RankOrderings.lean` (§2.F): - -- **§1.G** defines pairwise choice probabilities `P(x,y) = v(x)/(v(x)+v(y))`, - JND thresholds, the semiorder `(L(π), I(π))`, and the trace ordering. -- **§2.F** defines ranking probabilities as products of successive `pChoice` - values from shrinking alternative sets. - -The bridge connects them via five results: - -1. **`fromScale`**: Construct a `RationalAction` from a raw scale `v : A → ℝ`. -2. **`pairwiseProb_eq_pChoice`**: Binary choice probability equals `pChoice` - restricted to the pair `{x, y}`. -3. **`rankProbRec_swap_ratio`**: Swapping two adjacent elements in a ranking - changes the probability by the ratio `(v(x) + S_rest) / (v(y) + S_rest)`. -4. **JND effects on rankings**: Indistinguishable items have bounded swap - ratio; discriminable items have ordered ranking probability. -5. **Trace–expected rank**: The trace ordering matches expected rank ordering. --/ - -namespace Core - -open Real BigOperators Finset - -variable {A : Type*} [Fintype A] [DecidableEq A] - --- ============================================================================ --- §1. RationalAction from a ratio scale --- ============================================================================ - -/-- Construct a `RationalAction` from a raw positive scale `v : A → ℝ`, - the type used throughout ChoiceApproximations (§1.G). - - This lets us apply the RankOrderings (§2.F) machinery — `rankProbRec`, - `expectedRank` — to the same scales that define `pairwiseProb`, `jndL`, - `jndI`, and the trace. -/ -noncomputable def RationalAction.fromScale (v : A → ℝ) (hv : ∀ a, 0 ≤ v a) : - RationalAction Unit A where - score _ a := v a - score_nonneg _ a := hv a - --- ============================================================================ --- §2. pairwiseProb = pChoice on pairs --- ============================================================================ - -/-- The fundamental connection between §1.G and §2.F: binary choice - probability `P(x, y) = v(x)/(v(x)+v(y))` from ChoiceApproximations - equals `pChoice` from RationalAction on the two-element set `{x, y}`. - - Proof: unfold both sides. `pairwiseProb v x y = v x / (v x + v y)`. - `pChoice {x,y} x = v x / (∑ b ∈ {x,y}, v b) = v x / (v x + v y)` - when `x ≠ y` (so `{x,y}` has two elements). -/ -theorem pairwiseProb_eq_pChoice (v : A → ℝ) (hv : ∀ a, 0 < v a) - (x y : A) (hne : x ≠ y) : - pairwiseProb v x y = - (RationalAction.fromScale v (λ a => le_of_lt (hv a))).pChoice () {x, y} x := by - simp only [pairwiseProb, RationalAction.pChoice, RationalAction.fromScale] - have hx_mem : x ∈ ({x, y} : Finset A) := mem_insert_self x {y} - simp only [hx_mem, ↓reduceIte] - have hx_notin_y : x ∉ ({y} : Finset A) := by simp [hne] - have hsum_eq : ∑ b ∈ ({x, y} : Finset A), v b = v x + v y := - by rw [Finset.sum_insert hx_notin_y, Finset.sum_singleton] - have hsum_ne : ∑ b ∈ ({x, y} : Finset A), v b ≠ 0 := by - rw [hsum_eq]; linarith [hv x, hv y] - simp only [hsum_ne, ↓reduceIte] - rw [hsum_eq] - --- ============================================================================ --- §3. Adjacent-swap ranking ratio --- ============================================================================ - --- Private helpers for swap ratio proof - -private theorem pChoice_pos_of_score_pos (ra : RationalAction Unit A) (s : Unit) - (T : Finset A) (a : A) (ha : a ∈ T) (hpos : ∀ b, 0 < ra.score s b) : - 0 < ra.pChoice s T a := by - have hsum_pos : 0 < ∑ b ∈ T, ra.score s b := - Finset.sum_pos (fun b _ => hpos b) ⟨a, ha⟩ - simp only [RationalAction.pChoice, ha, ne_of_gt hsum_pos, ↓reduceIte] - exact div_pos (hpos a) hsum_pos - -private theorem rankProbRec_pos_of_score_pos (ra : RationalAction Unit A) (s : Unit) - (ranking : List A) (hpos : ∀ b, 0 < ra.score s b) : - 0 < rankProbRec ra s ranking := by - induction ranking with - | nil => simp [rankProbRec] - | cons a rest ih => - show 0 < ra.pChoice s (a :: rest).toFinset a * rankProbRec ra s rest - exact mul_pos - (pChoice_pos_of_score_pos ra s _ a (by simp [List.toFinset_cons]) hpos) ih - -private theorem pChoice_eq_score_div_sum (ra : RationalAction Unit A) (s : Unit) - (T : Finset A) (a : A) (ha : a ∈ T) - (hne : ∑ b ∈ T, ra.score s b ≠ 0) : - ra.pChoice s T a = ra.score s a / ∑ b ∈ T, ra.score s b := by - simp [RationalAction.pChoice, ha, hne] - -/-- Swapping two adjacent elements in a ranking changes the probability by - the ratio `(v(x) + S_rest) / (v(y) + S_rest)` where `S_rest = ∑ b ∈ rest, v b`. - - This corrects the naive intuition that the ratio should be `v(x)/v(y)`. - The difference arises because the *second* step of each ranking draws from - a different set: `{y} ∪ rest` vs `{x} ∪ rest`. Expanding: - - `rankProbRec(x::y::rest) / rankProbRec(y::x::rest)` - `= [pChoice(T, x) · pChoice({y}∪R, y)] / [pChoice(T, y) · pChoice({x}∪R, x)]` - `= [v(x)/S_T · v(y)/(v(y)+S_R)] / [v(y)/S_T · v(x)/(v(x)+S_R)]` - `= (v(x)+S_R) / (v(y)+S_R)` - - where `T = {x,y} ∪ R` and `S_R = ∑ b ∈ R, v b`. -/ -theorem rankProbRec_swap_ratio (ra : RationalAction Unit A) (s : Unit) - (x y : A) (rest : List A) (_hne : x ≠ y) - (hx : x ∉ rest) (hy : y ∉ rest) - (_hnd : rest.Nodup) - (hpos : ∀ b, 0 < ra.score s b) : - rankProbRec ra s (x :: y :: rest) / rankProbRec 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) := by - set vx := ra.score s x; set vy := ra.score s y - set S_R := ∑ b ∈ rest.toFinset, ra.score s b - set tail := rankProbRec ra s rest - have hvx := hpos x; have hvy := hpos y - have hS_nn : 0 ≤ S_R := Finset.sum_nonneg fun b _ => le_of_lt (hpos b) - have htail_pos := rankProbRec_pos_of_score_pos ra s rest hpos - have hx_notin : x ∉ rest.toFinset := by rwa [List.mem_toFinset] - have hy_notin : y ∉ rest.toFinset := by rwa [List.mem_toFinset] - have hT_eq : (x :: y :: rest).toFinset = (y :: x :: rest).toFinset := by - simp only [List.toFinset_cons]; ext a; simp [Finset.mem_insert]; tauto - show ra.pChoice s (x :: y :: rest).toFinset x * - (ra.pChoice s (y :: rest).toFinset y * tail) / - (ra.pChoice s (y :: x :: rest).toFinset y * - (ra.pChoice s (x :: rest).toFinset x * tail)) = - (vx + S_R) / (vy + S_R) - rw [hT_eq] - set T := (y :: x :: rest).toFinset - have hS_T_ne : ∑ b ∈ T, ra.score s b ≠ 0 := - ne_of_gt (Finset.sum_pos (fun b _ => hpos b) - ⟨y, by simp [T, List.toFinset_cons]⟩) - have hS_yR_ne : vy + S_R ≠ 0 := ne_of_gt (by linarith) - have hS_xR_ne : vx + S_R ≠ 0 := ne_of_gt (by linarith) - rw [pChoice_eq_score_div_sum ra s T x (by simp [T, List.toFinset_cons]) hS_T_ne, - pChoice_eq_score_div_sum ra s T y (by simp [T, List.toFinset_cons]) hS_T_ne, - pChoice_eq_score_div_sum ra s (y :: rest).toFinset y (by simp [List.toFinset_cons]) - (by rw [List.toFinset_cons, Finset.sum_insert hy_notin]; exact hS_yR_ne), - pChoice_eq_score_div_sum ra s (x :: rest).toFinset x (by simp [List.toFinset_cons]) - (by rw [List.toFinset_cons, Finset.sum_insert hx_notin]; exact hS_xR_ne)] - rw [show ∑ b ∈ (y :: rest).toFinset, ra.score s b = vy + S_R from - by rw [List.toFinset_cons, Finset.sum_insert hy_notin], - show ∑ b ∈ (x :: rest).toFinset, ra.score s b = vx + S_R from - by rw [List.toFinset_cons, Finset.sum_insert hx_notin]] - have hne_tail : (tail : ℝ) ≠ 0 := ne_of_gt htail_pos - field_simp - --- ============================================================================ --- §4. JND effects on ranking probability --- ============================================================================ - -/-- If `x` is discriminably preferred to `y` at threshold `π` (i.e., `xL(π)y`), - then the ranking with `x` before `y` is strictly more probable than - the ranking with `y` before `x`. - - From `jndL`, `P(x,y) > π > 1/2`, so `v(x) > v(y)`, hence - `v(x) + S_R > v(y) + S_R`, making the ranking `x::y::rest` more probable. - - This is the ranking-probability counterpart of Theorem 5's L-transitivity: - discriminable preference in pairwise choice implies discriminable - preference in ranking probability. -/ -theorem jndL_swap_ordered (v : A → ℝ) (hv : ∀ a, 0 < v a) (thr : ℝ) - (hthr_lower : 1 / 2 < thr) (x y : A) (rest : List A) - (hL : jndL v thr x y) - (hx : x ∉ rest) (hy : y ∉ rest) (hnd : rest.Nodup) : - rankProbRec (RationalAction.fromScale v (λ a => le_of_lt (hv a))) () - (y :: x :: rest) < - rankProbRec (RationalAction.fromScale v (λ a => le_of_lt (hv a))) () - (x :: y :: rest) := by - set ra := RationalAction.fromScale v (λ a => le_of_lt (hv a)) - have hpos : ∀ b, 0 < ra.score () b := fun b => hv b - have hne : x ≠ y := by - intro heq; subst heq - simp [jndL, pairwiseProb_self (hv x)] at hL; linarith - have hvxy : v y < v x := - (pairwiseProb_gt_half_iff (hv x) (hv y)).mp (lt_trans hthr_lower hL) - have hden_pos := rankProbRec_pos_of_score_pos ra () (y :: x :: rest) hpos - have hratio := rankProbRec_swap_ratio ra () x y rest hne hx hy hnd hpos - have hvy_S_pos : (0 : ℝ) < ra.score () y + ∑ b ∈ rest.toFinset, ra.score () b := - add_pos_of_pos_of_nonneg (hpos y) (Finset.sum_nonneg fun b _ => le_of_lt (hpos b)) - have h1 : 1 < rankProbRec ra () (x :: y :: rest) / rankProbRec ra () (y :: x :: rest) := by - rw [hratio, one_lt_div hvy_S_pos] - -- ra.score () x = v x and ra.score () y = v y - have : ra.score () y < ra.score () x := hvxy - linarith - exact (one_lt_div hden_pos).mp h1 - -/-- If `x` and `y` are indistinguishable at threshold `π` (i.e., `xI(π)y`), - then swapping them in a ranking changes the probability by at most - a factor of `thr / (1 - thr)`. - - From `jndI`, `P(x,y) ≤ thr`, so `v(x)/(v(x)+v(y)) ≤ thr`, giving - `v(x)/v(y) ≤ thr/(1-thr)`. Since `(v(x)+S_R)/(v(y)+S_R) ≤ v(x)/v(y)` - when `v(x) ≥ v(y)` (adding a constant to both sides shrinks the ratio), - the swap ratio is bounded by `thr/(1-thr)`. - - When `v(x) ≤ v(y)`, the ratio is ≤ 1 < thr/(1-thr) (since thr > 1/2). -/ -theorem jndI_swap_bounded (v : A → ℝ) (hv : ∀ a, 0 < v a) (thr : ℝ) - (hthr_lower : 1 / 2 < thr) (hthr_upper : thr < 1) (x y : A) (rest : List A) - (hI : jndI v thr x y) - (hx : x ∉ rest) (hy : y ∉ rest) (hnd : rest.Nodup) : - rankProbRec (RationalAction.fromScale v (λ a => le_of_lt (hv a))) () - (x :: y :: rest) / - rankProbRec (RationalAction.fromScale v (λ a => le_of_lt (hv a))) () - (y :: x :: rest) ≤ thr / (1 - thr) := by - set ra := RationalAction.fromScale v (λ a => le_of_lt (hv a)) - have hpos : ∀ b, 0 < ra.score () b := fun b => hv b - by_cases heq : x = y - · -- x = y: ratio is 1, and thr/(1-thr) ≥ 1 since thr > 1/2 - subst heq - rw [div_self (ne_of_gt (rankProbRec_pos_of_score_pos ra () (x :: x :: rest) hpos))] - rw [le_div_iff₀ (by linarith : (0:ℝ) < 1 - thr)] - linarith - · -- x ≠ y: use swap ratio - have hratio := rankProbRec_swap_ratio ra () x y rest heq hx hy hnd hpos - rw [hratio] - -- Convert ra.score to v for arithmetic - have hv_eq : ∀ b, ra.score () b = v b := fun _ => by - simp only [ra, RationalAction.fromScale] - simp_rw [hv_eq] - set S_R := ∑ b ∈ rest.toFinset, v b - have hS_nn : 0 ≤ S_R := Finset.sum_nonneg fun b _ => le_of_lt (hv b) - have h1thr : 0 < 1 - thr := by linarith - have hvy_S : 0 < v y + S_R := by linarith [hv y] - obtain ⟨_, hhi⟩ := hI - simp only [pairwiseProb] at hhi - have hvx_bound : v x * (1 - thr) ≤ thr * v y := by - have : v x ≤ thr * (v x + v y) := by - rwa [div_le_iff₀ (by linarith [hv x, hv y] : (0:ℝ) < v x + v y)] at hhi - nlinarith - suffices h : (v x + S_R) * (1 - thr) ≤ thr * (v y + S_R) from - (div_le_div_iff₀ hvy_S h1thr).mpr h - nlinarith [mul_nonneg hS_nn (show 0 ≤ 2 * thr - 1 from by linarith)] - --- ============================================================================ --- §5. Trace ordering matches expected rank ordering --- ============================================================================ - -/-- The trace ordering from §1.G (Definition 4) matches the expected rank - ordering from §2.F: `x ≥_T y` iff `E[rank(x)] ≤ E[rank(y)]`. - - By `trace_iff_scale_ge`, `x ≥_T y ↔ v(x) ≥ v(y)`. - By `expectedRank_lt_of_score_gt`, `v(x) > v(y)` implies - `E[rank(x)] < E[rank(y)]`. So the two orderings agree on strict preference. - - The `≤` case (when `v(x) = v(y)`) follows from `expectedRank_eq_of_score_eq`. -/ -theorem traceGe_iff_expectedRank_le (v : A → ℝ) (hv : ∀ a, 0 < v a) - (T : Finset A) (x y : A) (hx : x ∈ T) (hy : y ∈ T) (hne : x ≠ y) : - traceGe v x y ↔ - expectedRank (RationalAction.fromScale v (λ a => le_of_lt (hv a))) () T x ≤ - expectedRank (RationalAction.fromScale v (λ a => le_of_lt (hv a))) () T y := by - set ra := RationalAction.fromScale v (λ a => le_of_lt (hv a)) - have hpos' : ∀ a ∈ T, 0 < ra.score () a := fun a _ => hv a - constructor - · -- Forward: traceGe → v(y) ≤ v(x) → E[rank(x)] ≤ E[rank(y)] - intro h - rw [trace_iff_scale_ge v hv x y] at h - rcases eq_or_lt_of_le h with heq | hlt - · -- v(y) = v(x): equal scores → equal expected ranks - exact le_of_eq (expectedRank_eq_of_score_eq ra () T x y hx hy hne hpos' heq.symm) - · -- v(y) < v(x): strict monotonicity - exact le_of_lt (expectedRank_lt_of_score_gt ra () T x y hx hy hne hpos' hlt) - · -- Backward: E[rank(x)] ≤ E[rank(y)] → traceGe (contrapositive) - intro hle - rw [trace_iff_scale_ge v hv x y] - by_contra h_not - push Not at h_not - -- h_not : v x < v y, i.e., ra.score () y > ra.score () x - have hgt : ra.score () y > ra.score () x := h_not - have := expectedRank_lt_of_score_gt ra () T y x hy hx hne.symm hpos' hgt - linarith - -end Core diff --git a/Linglib/Studies/CohnGordonEtAl2019.lean b/Linglib/Studies/CohnGordonEtAl2019.lean index cb57ac354..5d7a09d40 100644 --- a/Linglib/Studies/CohnGordonEtAl2019.lean +++ b/Linglib/Studies/CohnGordonEtAl2019.lean @@ -1,7 +1,6 @@ import Linglib.Pragmatics.RSA.LatentOperators import Linglib.Pragmatics.RSA.Operators import Linglib.Core.Probability.Scores -import Linglib.Core.Probability.Choice.RationalAction import Linglib.Processing.VisualWorld import Linglib.Studies.SedivyEtAl1999 diff --git a/Linglib/Studies/EgreEtAl2023.lean b/Linglib/Studies/EgreEtAl2023.lean index de31423f0..6d03767ff 100644 --- a/Linglib/Studies/EgreEtAl2023.lean +++ b/Linglib/Studies/EgreEtAl2023.lean @@ -1,4 +1,4 @@ -import Linglib.Core.Probability.Choice.RationalAction +import Linglib.Core.Probability.LogitChoice import Linglib.Pragmatics.RSA.Operators import Mathlib.Data.Rat.Defs import Mathlib.Data.Fintype.BigOperators diff --git a/blog/references.bib b/blog/references.bib index 114038c24..18e3e00b1 100644 --- a/blog/references.bib +++ b/blog/references.bib @@ -1418,6 +1418,33 @@ @book{luce-1959 role = {foundational}, sources = {Core/Probability/Choice/RationalAction.lean;Studies/Luce1959.lean} } +@article{plackett-1975, + author = {Plackett, R. L.}, + year = {1975}, + title = {The Analysis of Permutations}, + journal = {Journal of the Royal Statistical Society. Series C (Applied Statistics)}, + volume = {24}, + number = {2}, + pages = {193--202}, + doi = {10.2307/2346567}, + subfield = {pragmatics/rsa}, + validated = {true}, + role = {cited}, + sources = {Core/Probability/Choice/RankOrderings.lean} +} +@book{marden-1995, + author = {Marden, John I.}, + year = {1995}, + title = {Analyzing and Modeling Rank Data}, + publisher = {Chapman \& Hall}, + address = {London}, + series = {Monographs on Statistics and Applied Probability}, + number = {64}, + subfield = {pragmatics/rsa}, + validated = {true}, + role = {cited}, + sources = {Core/Probability/Choice/RankOrderings.lean} +} @book{ludeling-2001, author = {Lüdeling, Anke}, year = {2001},