Lemma 1 — consequences of (IC) and (FC) along unilateral deviations

A principal allocates one good among $I\ge2$ agents $i\in\mathcal I$. Agent $i$ has a type $t_i\in\mathcal T_i=[\underline t_i,\overline t_i]$ with $0\le\underline t_i<\overline t_i$, and inspecting agent $i$ costs $c_i>0$. Write $\mathcal T=\prod_i\mathcal T_i$ and $\mathcal X$ for the feasible mechanisms of (MDP).

Let $(p,q)\in\mathcal X$, $i\in\mathcal I$ and $t\in\mathcal T$. A scenario $(t'_i,t_{-i})$ with $t'_i\in\mathcal T_i$ is called $i$-unilaterally reachable from $t$.

1. If $p_i(t)-q_i(t)=1$, then $p_i(t'_i,t_{-i})=1$ for all $t'_i\in\mathcal T_i$: if agent $i$ gets the good without inspection in $t$, he gets it in every $i$-unilaterally reachable scenario.
2. If $p_i(t)=0$, then $p_i(t'_i,t_{-i})=q_i(t'_i,t_{-i})$ for all $t'_i\in\mathcal T_i$: if agent $i$ does not get the good in $t$, he is inspected whenever he wins in an $i$-unilaterally reachable scenario.

These two facts are the non-local consequences of (IC) that drive the spatial induction behind Proposition 1 and Lemma 4.

Differences from the source:

• encoding: agents I = {1,…,I} with I ≥ 2 → a finite type ι with 2 ≤ Fintype.card ι; reason: relabelling of the agents; same instances
• encoding: mechanisms with p_i, q_i ∈ L(𝒯,[0,1]) (bounded Borel functions on 𝒯) → p q : ι → (ι → ℝ) → ℝ, Borel measurable on ℝ^ι, with [0,1] bounds required only on 𝒯; reason: every Borel function on the closed box 𝒯 extends to a Borel function on ℝ^ι; all notions depend only on the values on 𝒯
• encoding: the scenario (t′ᵢ, t₋ᵢ) → Function.update t i t′ᵢ; reason: same vector