Kemperman–Scherk: $|A_1+\cdots+A_m| \ge |A_1|+\cdots+|A_m|-(m-1)$

Let $G$ be an abelian group and let $A_1, \ldots, A_m$ be finite subsets of $G$, each containing $0$. Assume that $0$ has only the trivial representation in the sumset, that is, whenever $x_j \in A_j$ for $j = 1, \ldots, m$ and

one necessarily has $x_1 = x_2 = \cdots = x_m = 0$. Then

For $m = 2$ this is the classical addition theorem of P. Scherk and J. H. B. Kemperman; the general $m$ is obtained from it by induction, and is stated as Corollary 4 by Erdős, Lev, Rauzy, Sándor and Sárközy. The result says that a sumset in which $0$ is represented only trivially cannot be much smaller than the largest of its summands; it is the tool that lets one add up lower bounds for several sets of subset sums without losing more than $m-1$ elements in total.

Formalization Note The $m$-fold sumset $A_1 + \cdots + A_m$ is rendered as the image of the dependent product $\prod_j A_j$ (Fintype.piFinset) under the map $f \mapsto \sum_j f(j)$, and the summands are indexed by Fin m. Because the cardinalities are natural numbers, the conclusion is stated in the subtraction-free form $\sum_j |A_j| \le |A_1 + \cdots + A_m| + (m-1)$, which is equivalent to the displayed inequality and also correct at $m = 0$.