The number of subset sums is monotone under inclusion

Proved

Erdos131.card_subsetSums_mono

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

additive-combinatoricscombinatoricserdos-problemsgroup-theory

Let $G$ be an abelian group and let $B \subseteq A$ be finite subsets of $G$ . Write

\mathcal{P}(X) \ = \ \Big\{ \textstyle\sum_{x \in S} x \ : \ S \subseteq X \Big\}

for the set of subset sums of a finite set $X$ , the empty subset contributing $0$ . Then

|\mathcal{P}(B)| \ \le \ |\mathcal{P}(A)| .

The content is only that every subset of $B$ is a subset of $A$ , so $\mathcal{P}(B) \subseteq \mathcal{P}(A)$ and the cardinalities compare. It is recorded because every lower bound for the number of subset sums — the trivial bound $|A|+1$ , or Olson's $1 + |A|^2/9$ — is applied in practice to a conveniently chosen subset of the set one actually cares about, and this is the step that transports the resulting bound back up.

Formalization Note. Throughout, the set of subset sums of a finite set $A$ in an abelian group is rendered as A.powerset.image (fun S => ∑ x ∈ S, x), the image of the powerset of $A$ under the summation map. The empty subset is included, so $0$ always belongs to it. No hypothesis is placed on $A$ or $B$ ; both may be empty, in which case both sides equal $1$ .

Preamble

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

Formal statement

theorem Erdos131.card_subsetSums_mono {G : Type*} [AddCommGroup G] [DecidableEq G]
    {A B : Finset G} (h : B ⊆ A) :
    (B.powerset.image fun S => ∑ x ∈ S, x).card
      ≤ (A.powerset.image fun S => ∑ x ∈ S, x).card := by sorry

Source

Auxiliary infrastructure for Erdős problem #131 (https://www.erdosproblems.com/131). These statements are elementary structural facts about the set of subset sums, stated for this formalization rather than quoted verbatim; they are the manipulations used implicitly in Section 5 of 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: https://math.haifa.ac.il/seva/Papers/greeda.dvi), in the proofs of their Theorem 3 and in J. E. Olson, 'Sums of sets of group elements', Acta Arith. 28 (1975), 147-156.

View graph