Sidon

1 Basic Sidon sets results

Definition 1 Sidon set
✓
#

Lean declarations

A set \(S \subseteq M\), where \(M\) is an additive commutative monoid, is called a Sidon set if for all \(a, b, c, d \in S\), then \(a + b = c + d \implies \{ a, b\} = \{ c, d\} \), that is, there are no repeated sums.

Theorem 2
✓
#

Uses

Lean declarations

The empty set is a Sidon set.

Theorem 3
✓
#

Uses

Lean declarations

A singleton set is a Sidon set.

Theorem 4
✓
#

Uses

Lean declarations

If \(S\) is a Sidon set and \(T \subseteq S\), then \(T\) is a Sidon set.

Theorem 5
#

Uses

Lean declarations

If \(S\) is a Sidon set in a finite additive commutative group \(M\), then \(|S| \cdot (|S| - 1) \leq |M|\).

Proof ▶

Let \(S = \{ a_1, \ldots , a_n\} \). Consider the differences \(a_i - a_j\) for \(i \neq j\). Since \(S\) is Sidon, theses differences are unique, and there are at most \(|M|\) of them. By injectivity, the proof follows.