From 9b26f56120422dec9537505f3971ce67dd46c68f Mon Sep 17 00:00:00 2001
From: Thibaut Horel <thibaut.horel@gmail.com>
Date: Sat, 6 Jul 2013 15:54:48 +0200
Subject: Add proof of Myerson's lemma. Introduce the counterexample in the
 body.

---
 myerson.tex | 28 ++++++++++++++++++++++++++++
 1 file changed, 28 insertions(+)

(limited to 'myerson.tex')

diff --git a/myerson.tex b/myerson.tex
index 8b13789..bcfedc4 100644
--- a/myerson.tex
+++ b/myerson.tex
@@ -1 +1,29 @@
+Using the notations of Lemma~\ref{thm:myerson-variant}, we want to prove that
+if $c_i$ and $c_i'$ are two different costs reported by user $i$ with $|c_i
+- c_i'|\geq \delta$, and if $c_{-i}$ is any vector of costs reported by the
+other users:
+\begin{equation}\label{eq:local-foobar}
+    p_i(c_i, c_{-i}) - s_i(c_i, c_{-i})\cdot c_i \geq p_i(c_i', c_{-i})
+    - s_i(c_i', c_{-i})\cdot c_i
+\end{equation}
 
+We distinguish four cases depending on the value of $s_i(c_i, c_{-i})$ and
+$s_i'(c_i', c_{-i})$.
+
+Since the mechanism is normalized, if $s_i(c_i, c_{-i})= s_i(c_i', c_{-i})=0$,
+we have $p_i(c_i, c_{-i}) = p_i(c_i', c_{-i})= 0$ and \eqref{eq:local-foobar}
+is true.
+
+Note that $i$ is paid her threshold payment when allocated, and since this
+payment does not depend on $i$'s reported cost, \eqref{eq:local-foobar} is true
+(and is in fact an equality) when $s_i(c_i', c_{-i}) = s_i(c_i, c_{-i}) = 1$.
+
+If $s_i(c_i', c_{-i}) = 0$ and $s_i(c_i, c_{-i}) = 1$, we have $p_i(c_i',
+c_{-i}) = 0$ by normalization and \eqref{eq:local-foobar} follows from
+individual rationality.
+
+Finally, let us assume that $s_i(c_i', c_{-i}) = 1$ and $s_i(c_i, c_{-i}) = 0$.
+By $\delta$-decreasingness of $s_i$, $c_i \geq c_i'+\delta$, and $s_i(c_i,
+c_{-i}) = 0$ implies that $i$'s threshold payment is less than $c_i$,
+\emph{i.e.} $p_i(c_i', c_{-i}) \leq c_i$. This last inequality is equivalent to
+\eqref{eq:local-foobar} in this final case.
-- 
cgit v1.2.3-70-g09d2

