Kemperman--Wehn addition theorem: $|A|+|B| \le |A+B| + r_{A,B}(c)$

Proved

Erdos131.olson_thm2_1

by moutei · Sep 22, 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 non-empty sets. For $c \in G$ write

r_{A,B}(c) \ = \ \#\{(a,b) \in A \times B \ : \ a + b = c\}

for the number of representations of $c$ as a sum of an element of $A$ and an element of $B$ . The theorem asserts that the sumset cannot be small unless every one of its elements is represented many times: if

|A+B| \ = \ |A| + |B| - k,

then every $c \in A + B$ satisfies $r_{A,B}(c) \ge k$ . Equivalently, and this is the form stated here,

|A| + |B| \ \le \ |A+B| + r_{A,B}(c) \qquad \text{for every } c \in A + B.

This is the addition theorem of Kemperman and Wehn, going back to L. Moser and P. Scherk in the abelian case. It is the representation-counting strengthening of the Kemperman--Scherk inequality: the familiar conclusion $|A+B| \ge |A| + |B| - 1$ is what one gets by feeding in a single element with a unique representation, whereas the statement above extracts a lower bound on the representation count of each element of the sumset from the size of the sumset alone.

Relation to the mission's existing card. refErdos131.kemperman_scherk_two is the special case $k = 1$ , normalised by translation so that the distinguished element is $c = 0$ and its unique representation is $0 = 0 + 0$ . The present statement is strictly stronger: it applies at every $c$ simultaneously and with every $k$ .

Sharpness. Equality holds whenever $A = B = H$ for a finite subgroup $H$ : then $A + B = H$ , so $k = |A| + |B| - |A+B| = |H|$ , and indeed each $c \in H$ has exactly $|H|$ representations $c = a + (c-a)$ . Equality also holds for arithmetic progressions with a common difference, where $k = 1$ and the two endpoints of the sumset have unique representations.

Formalization notes.

Subtraction-free form. Finset.card takes values in $\mathbb{N}$ , where subtraction truncates, so the source's parameter $k$ is not introduced; instead the conclusion is stated as $|A| + |B| \le |A+B| + r_{A,B}(c)$ . This is equivalent to the source: taking $k = |A| + |B| - |A+B|$ , which is the largest admissible value and the one the source's equation pins down, recovers Olson's wording, and for any smaller $k$ the source's conclusion is weaker than the displayed inequality.

Commutativity. Olson states Theorem 2.1 for an arbitrary, not necessarily abelian, group; the paper's introduction is explicit that this is the generality it works in. The card records the abelian case, [AddCommGroup G], which is the case consumed by the rest of this mission. The non-abelian statement is a genuinely stronger result and would need a separate card.

Hypotheses. The non-emptiness hypotheses hA and hB are the source's own and are kept, even though both already follow from hc : c ∈ A + B.

Representation count. $r_{A,B}(c)$ is rendered as ((A ×ˢ B).filter (fun p => p.1 + p.2 = c)).card, the number of pairs $(a,b)$ , which is what "representations $c = a+b$ with $a \in A$ , $b \in B$ " means in the source.

Preamble

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

Formal statement

theorem Erdos131.olson_thm2_1 {G : Type*} [AddCommGroup G] [DecidableEq G]
    (A B : Finset G) (hA : A.Nonempty) (hB : B.Nonempty) (c : G) (hc : c ∈ A + B) :
    A.card + B.card ≤ (A + B).card + ((A ×ˢ B).filter (fun p => p.1 + p.2 = c)).card := by sorry

Source

J. E. Olson, 'Sums of sets of group elements', Acta Arith. 28 (1975), 147-156. Open-access scan: http://matwbn.icm.edu.pl/ksiazki/aa/aa28/aa2825.pdf ; EUDML record https://eudml.org/doc/205377 . Page 147 (end) to page 148 (top), THEOREM 2.1 (Kemperman, Wehn), verbatim: 'Let A and B be finite non-empty subsets of G and let |A+B| = |A|+|B|-k. Then every element c in A+B has at least k representations as a sum c = a+b with a in A, b in B.' Olson adds: 'Theorem 2.1 goes back to results of L. Moser and P. Scherk in the case of abelian groups, and was proved for non-abelian groups by J. H. B. Kemperman and (independently) D. F. Wehn. For proof see Kemperman's paper [2].' Reference [2] is J. H. B. Kemperman, 'On complexes in a semigroup', Indag. Math. 18 (1956), 247-254. The card formalises the abelian case, in the subtraction-free form |A|+|B| <= |A+B| + r_{A,B}(c).

View graph

Kemperman--Wehn addition theorem: ∣A∣+∣B∣≤∣A+B∣+rA,B(c)|A|+|B| \le |A+B| + r_{A,B}(c)∣A∣+∣B∣≤∣A+B∣+rA,B​(c)

Kemperman--Wehn addition theorem: $|A|+|B| \le |A+B| + r_{A,B}(c)$