Subadditivity of the translation gain $\Delta_S(x)=|(x+S)\setminus S|$

Proved

Erdos131.card_translate_sdiff_subadditive

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

additive-combinatoricscombinatoricsgroup-theory

Let $G$ be an abelian group and let $S \subseteq G$ be finite. For $x \in G$ write

\Delta_S(x) \ = \ \bigl|(x + S) \setminus S\bigr|

for the number of elements that translating $S$ by $x$ moves out of $S$ ; equivalently $\Delta_S(x) = |S| - |(x+S) \cap S|$ , and in a finite ambient group $\Delta_S(x) = |(S+x) \cap \overline{S}|$ . Then $\Delta_S$ is subadditive:

\Delta_S(x + y) \ \le \ \Delta_S(x) + \Delta_S(y) \qquad \text{for all } x, y \in G .

The proof is the one-line containment

(x+y+S) \setminus S \ \subseteq \ \bigl((x+y+S) \setminus (y+S)\bigr) \ \cup \ \bigl((y+S) \setminus S\bigr),

together with the observation that $(x+y+S)\setminus(y+S)$ is the translate by $y$ of $(x+S)\setminus S$ and therefore has the same cardinality.

This is the quantity Olson calls $\lambda(g) = |(B+g) \cap \overline{B}|$ in Section 4 of his 1975 paper, and its subadditivity is exactly what lets one transfer a large gain from an iterated sumset element $d = c_1 + \cdots + c_n$ back to a single generator $c_i$ . It is the elementary half of Olson's Lemma 3.1 and of the corresponding step in the modern treatment of DeVos-Goddyn-Mohar-Šámal.

Formalization note. The translate $x + S$ is written as S.image fun s => x + s, matching the notation used elsewhere in this mission for $a + \mathcal{P}(A)$ . No finiteness of $G$ is needed.

Preamble

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

Formal statement

theorem Erdos131.card_translate_sdiff_subadditive {G : Type*} [AddCommGroup G] [DecidableEq G]
    (S : Finset G) (x y : G) :
    ((S.image fun s => (x + y) + s) \ S).card
      ≤ ((S.image fun s => x + s) \ S).card + ((S.image fun s => y + s) \ S).card := by sorry

Source

J. E. Olson, 'Sums of sets of group elements', Acta Arith. 28 (1975), 147-156, Section 4 (subadditivity of lambda(g) = |(B+g) cap complement(B)|, used in the proof of Lemma 3.1); the same statement appears as Observation 2.3, attributed to Erdos-Heilbronn, in M. DeVos, L. Goddyn, B. Mohar, R. Samal, 'A quadratic lower bound for subset sums', Acta Arith. 129 (2007), 187-195, arXiv:math/0612045, p. 6.

View graph

Subadditivity of the translation gain ΔS(x)=∣(x+S)∖S∣\Delta_S(x)=|(x+S)\setminus S|ΔS​(x)=∣(x+S)∖S∣

Subadditivity of the translation gain $\Delta_S(x)=|(x+S)\setminus S|$