Inequality (2) — the greedy deviation dominates each Algorithm 3-renamed good of Y_ℓ marginally

Let $\succ$ be a profile of rankings over $m=kn$ goods, $i$ an agent with valuation $v_i$, and $\succ'_i$ a greedy response of $i$ to $\succ_{-i}$ (Algorithm 4). Let $x_r$ be the good agent $i$ receives in round $r$ of Round-Robin$(\succ'_i,\succ_{-i})$, so that $A'_i=\{x_1,\dots,x_k\}$. For an agent $j\ne i$ list its bundle $A_j$ in Round-Robin$(\succ)$ as $y_1,\dots,y_k$ in order of allocation in Round-Robin$(\succ'_i,\succ_{-i})$, form $Y_1=\{y_3,y_5,\dots\}$ and $Y_2=\{y_2,y_4,\dots\}$, and for $\ell\in\{1,2\}$ rename $Y_\ell=\{y^\ell_1,\dots,y^\ell_{\tau_\ell}\}$ by Algorithm 3 with inputs $A'_i$, $Y_\ell$, $v_i$. Then for $\ell\in\{1,2\}$ and $r\in[\tau_\ell]$,

Inequality (2) is the good-by-good comparison that, summed over $r$ and combined with submodularity, bounds $v_i(A_j\setminus\{y_1\})$ by three times $v_i(A'_i)$ in the closing bound.

Formalization Note The greedy response and Algorithm 3 are encoded relationally (IsGreedyResponse, IsAlg3Order), so the statement covers every tie-breaking. The hypothesis hx identifies x r (0-based round r) with the good picked at step r*n + i of the deviation run, and Y is either Yone y k or Ytwo y k. No equilibrium hypothesis and no property of $v_i$ is assumed: the argument of p. 20 uses only the greedy choice, the Algorithm 3 order and the parity split, so the Lean statement holds for an arbitrary real set function $v_i$, which is stronger than the paper's setting. 0-based: y' r is the paper's $y^\ell_{r+1}$ and (Finset.range r).image x is $\{x_1,\dots,x_r\}$ in the paper's indexing, i.e. the goods $i$ received before its $(r+1)$-st pick.

Formalization Note Agents are Fin n with $n\ge1$ (0-based: the paper's agent $i$ is i - 1), goods a finite type $M$ with $|M| = m$, and the paper's standing simplification $m = kn$ (p. 7) is the hypothesis hm : Fintype.card M = k * n; the paper calls it without loss of generality (dummy goods), and that reduction is not formalized. Steps of Round-Robin are 0-based: the paper's step $(r-1)n+i$ is step (r-1)*n + (i-1), and the paper's $S_r$, $S'_r$ (goods allocated in steps $1,\dots,rn+i-1$) are allocBefore σ (r*n + i) and allocBefore (Function.update σ i τ) (r*n + i) for the 0-based agent i. A ranking is a duplicate-free list of all goods; the deviating profile $(\succ'_i,\succ_{-i})$ is Function.update σ i τ.