Olson (32): $\sum_{c\in C}|(S+c)\setminus S|\ge|C||S|-|S|(|S|-1)$ for $0\notin C$

Let $G$ be an abelian group, let $S\subseteq G$ be finite, and let $C\subseteq G$ be a finite set of non-zero elements. Write

for the number of points by which the translate $S+c$ sticks out of $S$. Then

This is equation (32) in the proof of Olson's Lemma 3.1 (Acta Arith. 28 (1975), p. 155). Olson writes it as

the point being that the correlation sum is taken over non-zero shifts only, where $\sum_{x\neq 0}|(S+x)\cap S|=|S|(|S|-1)$ rather than $\sum_{x\in G}|(S+x)\cap S|=|S|^2$. For $|C|=2k-1$ and $|S|=k$ it gives $\sum_{c\in C}\lambda(c)\ge k^2$, which is exactly what Case 1 of Olson's Lemma 3.1 needs; the weaker bound coming from the sum over all of $G$ loses a factor $|S|$ and yields only $k(k-1)$.

Proof idea. Fix $x\in S$. The map $c\mapsto c+x$ is injective and sends $\{c\in C: c+x\in S\}$ into $S\setminus\{x\}$, because $c\neq 0$ forces $c+x\neq x$. Hence $\#\{c\in C:c+x\in S\}\le |S|-1$, and summing over $x\in S$ after exchanging the order of summation bounds $\sum_{c\in C}|(S+c)\cap S|$ by $|S|(|S|-1)$.

Formalisation notes. The statement is written subtraction-free, C.card * S.card + S.card ≤ S.card * S.card + ∑ c ∈ C, ((S.image fun s => c + s) \ S).card, because Finset.card lands in $\mathbb N$ and truncated subtraction would change the meaning when $|C||S|<|S|(|S|-1)$; adding $|S|$ to both sides of Olson's inequality and moving $|S|^2$ to the right gives the displayed form. The translate is written S.image fun s => c + s, matching the existing infrastructure cards for $\lambda$. No finiteness of $G$ is assumed: unlike the averaging form obtained from a sum over the whole group, this count never needs $G$ finite, which is what makes it applicable to Olson's Lemma 3.1 where the ambient group may be infinite. Both $S=\emptyset$ and $C=\emptyset$ are allowed and the inequality is then trivially true.