Kemperman–Scherk addition theorem: $|A+B| \ge |A|+|B|-1$

Proved

Erdos131.kemperman_scherk_two

by moutei · Sep 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

additive-combinatoricscombinatoricserdos-problemsgroup-theory

Let $G$ be an abelian group and let $A, B \subseteq G$ be finite sets with $0 \in A \cap B$ . Assume that $0$ has only the trivial representation in the sumset $A + B$ , that is, whenever $a \in A$ , $b \in B$ and

a + b = 0,

one necessarily has $a = b = 0$ . Then

|A + B| \ \ge \ |A| + |B| - 1.

This is the addition theorem originating in the work of P. Scherk and J. H. B. Kemperman. The hypothesis says exactly that $A \cap (-B) = \{0\}$ , and it is what rules out the obvious obstruction: if $H$ is a finite subgroup and $A = B = H$ , then $|A + B| = |H|$ is far below $|A| + |B| - 1$ , but then every $a \in H$ contributes a representation $a + (-a) = 0$ .

The bound is sharp: for $A = B = \{0, 1\} \subseteq \mathbb{Z}$ one has $|A + B| = 3 = |A| + |B| - 1$ , and more generally equality holds for arithmetic progressions with a common difference.

In the general Kemperman–Scherk theorem the conclusion is $|A + B| \ge |A| + |B| - \min_{c \in A + B} r_{A,B}(c)$ , where $r_{A,B}(c)$ counts the representations $c = a + b$ ; the form above is the case where some element has a unique representation, normalised by translation so that this element is $0$ and the unique representation is $0 = 0 + 0$ . It is this normalised form that Erdős, Lev, Rauzy, Sándor and Sárközy quote as their Theorem 8 and then extend by induction to $m$ summands.

Formalization note. Because Finset.card takes values in $\mathbb{N}$ , where subtraction truncates, the conclusion is stated in the subtraction-free form

|A| + |B| \ \le \ |A + B| + 1,

which is equivalent to the displayed inequality. The sumset is Mathlib's pointwise A + B on Finset G, so the preamble opens the Pointwise scope. Both memberships $0 \in A$ and $0 \in B$ are kept as separate hypotheses, matching the source's $0 \in A \cap B$ ; neither follows from the uniqueness hypothesis, which is vacuous when $A$ or $B$ is empty.

Preamble

import Definitions.Def_Erdos131_NonDividing
import Mathlib.Tactic
open Erdos131
open scoped Pointwise

Formal statement

theorem Erdos131.kemperman_scherk_two {G : Type*} [AddCommGroup G] [DecidableEq G]
    (A B : Finset G) (hA : (0 : G) ∈ A) (hB : (0 : G) ∈ B)
    (huniq : ∀ a ∈ A, ∀ b ∈ B, a + b = 0 → a = 0 ∧ b = 0) :
    A.card + B.card ≤ (A + B).card + 1 := by sorry

Source

P. Erdős, V. Lev, G. Rauzy, C. Sándor, A. Sárközy, 'Greedy algorithm, arithmetic progressions, subset sums and divisibility', Discrete Math. 200 (1999), 119-135; author's preprint at https://math.haifa.ac.il/seva/Papers/greeda.dvi, Section 5, Theorem 8 (preprint p. 9): 'Let A and B be two subsets of an abelian group G such that 0 in A cap B, and suppose that the only representation of 0 in A + B is the trivial one: 0 = 0 + 0. Then |A + B| >= |A| + |B| - 1.' The authors attribute it to P. Scherk and J.H.B. Kemperman; see P. Scherk, 'Distinct elements in a set of sums', Amer. Math. Monthly 62 (1955), 46 (reference [22] of the paper).

View graph

Kemperman–Scherk addition theorem: ∣A+B∣≥∣A∣+∣B∣−1|A+B| \ge |A|+|B|-1∣A+B∣≥∣A∣+∣B∣−1

Kemperman–Scherk addition theorem: $|A+B| \ge |A|+|B|-1$