Olson (30) iterated: $c\in nA\Rightarrow\lambda(c)\le n\alpha$

Let $G$ be an abelian group, $S\subseteq G$ finite, and write $\lambda_S(g)=|(S+g)\setminus S|$. Let $A\subseteq G$ be finite with $0\in A$, and suppose

Then for every $n\ge 0$ and every $c$ in the $n$-fold sumset $nA=A+\cdots+A$,

This is the sentence "since $c\in nA$ implies $\lambda(c)\le n\alpha$ by (30)" in the proof of Olson's Lemma 3.1 (Acta Arith. 28 (1975), p. 155), which is what lets the shell decomposition of $rA$ be summed: an element reached in $n$ steps from $A$ costs at most $n$ times the maximum $\alpha=\max_i\lambda(a_i)$. Equation (30) itself is the subadditivity $\lambda(x+y)\le\lambda(x)+\lambda(y)$.

Proof idea. Induction on $n$. For $n=0$ the sumset $0A$ is $\{0\}$ and $\lambda_S(0)=0$. For the step, $(n+1)A=nA+A$, so $c=x+a$ with $x\in nA$ and $a\in A$, and subadditivity gives $\lambda_S(c)\le\lambda_S(x)+\lambda_S(a)\le n\alpha+\alpha$.

Formalisation notes. The $n$-fold sumset is the pointwise n • A of Finset G under open scoped Pointwise, which is the iterated sumset $A+\cdots+A$ (not the dilate $\{na : a\in A\}$); the convention 0 • A = {0} is what makes the base case true. The hypothesis $0\in A$ is Olson's standing assumption on $A=\{0,a_1,\dots,a_w\}$ in §4 and is kept for faithfulness to the source, but it is not used in the proof: the bound holds for any finite $A$, and with $0\in A$ it additionally means the shells $nA$ increase. The bound is stated with an arbitrary natural number $\alpha$ satisfying $\lambda_S(a)\le\alpha$ on $A$ rather than with the maximum itself, so that it can be applied to any upper bound for the $\lambda_S(a_i)$.