The Cauchy-Davenport theorem

This file proves a generalisation of the Cauchy-Davenport theorem to arbitrary groups.

Cauchy-Davenport provides a lower bound on the size of s + t in terms of the sizes of s and t, where s and t are nonempty finite sets in a monoid. Precisely, it says that |s + t| ≥ |s| + |t| - 1 unless the RHS is bigger than the size of the smallest nontrivial subgroup (in which case taking s and t to be that subgroup would yield a counterexample). The motivating example is s = {0, ..., m}, t = {0, ..., n} in the integers, which gives s + t = {0, ..., m + n} and |s + t| = m + n + 1 = |s| + |t| - 1.

There are two kinds of proof of Cauchy-Davenport:

• The first one works in linear orders by writing a₁ < ... < aₖ the elements of s, b₁ < ... < bₗ the elements of t, and arguing that a₁ + b₁ < ... < aₖ + b₁ < ... < aₖ + bₗ are distinct elements of s + t.
• The second one works in groups by performing an "e-transform". In an abelian group, the e-transform replaces s and t by s ∩ g • s and t ∪ g⁻¹ • t. For a suitably chosen g, this decreases |s + t| and keeps |s| + |t| the same. In a general group, we use a trickier e-transform (in fact, a pair of e-transforms), but the idea is the same.

Main declarations

• Finset.min_le_card_mul: A generalisation of the Cauchy-Davenport theorem to arbitrary groups.
• Monoid.IsTorsionFree.card_add_card_sub_one_le_card_mul: The Cauchy-Davenport theorem in torsion-free groups.
• ZMod.min_le_card_add: The Cauchy-Davenport theorem.
• Finset.card_add_card_sub_one_le_card_mul: The Cauchy-Davenport theorem in linear ordered cancellative semigroups.

TODO

Version for circle.

References

• Matt DeVos, On a generalization of the Cauchy-Davenport theorem

Tags

additive combinatorics, number theory, sumset, cauchy-davenport

General case

theorem Finset.min_le_card_add {α : Type u_1} [AddGroup α] [DecidableEq α] {s : Finset α} {t : Finset α} (hs : s.Nonempty) (ht : t.Nonempty) : min (AddMonoid.minOrder α) ↑(s.card + t.card - 1) ≤ ↑(s + t).card

A generalisation of the Cauchy-Davenport theorem to arbitrary groups. The size of s + t is lower-bounded by |s| + |t| - 1 unless this quantity is greater than the size of the smallest subgroup.

theorem Finset.min_le_card_mul {α : Type u_1} [Group α] [DecidableEq α] {s : Finset α} {t : Finset α} (hs : s.Nonempty) (ht : t.Nonempty) : min (Monoid.minOrder α) ↑(s.card + t.card - 1) ≤ ↑(s * t).card

A generalisation of the Cauchy-Davenport theorem to arbitrary groups. The size of s * t is lower-bounded by |s| + |t| - 1 unless this quantity is greater than the size of the smallest subgroup.

theorem AddMonoid.IsTorsionFree.card_add_card_sub_nonneg_card_add {α : Type u_1} [AddGroup α] [DecidableEq α] {s : Finset α} {t : Finset α} (h : AddMonoid.IsTorsionFree α) (hs : s.Nonempty) (ht : t.Nonempty) : s.card + t.card - 1 ≤ (s + t).card

The Cauchy-Davenport theorem for torsion-free groups. The size of s + t is lower-bounded by |s| + |t| - 1.

theorem Monoid.IsTorsionFree.card_add_card_sub_one_le_card_mul {α : Type u_1} [Group α] [DecidableEq α] {s : Finset α} {t : Finset α} (h : Monoid.IsTorsionFree α) (hs : s.Nonempty) (ht : t.Nonempty) : s.card + t.card - 1 ≤ (s * t).card

The Cauchy-Davenport Theorem for torsion-free groups. The size of s * t is lower-bounded by |s| + |t| - 1.

$$ℤ/nℤ$$

theorem ZMod.min_le_card_add {p : ℕ} (hp : Nat.Prime p) {s : Finset (ZMod p)} {t : Finset (ZMod p)} (hs : s.Nonempty) (ht : t.Nonempty) : min p (s.card + t.card - 1) ≤ (s + t).card

The Cauchy-Davenport Theorem. If s, t are nonempty sets in $$ℤ/pℤ$$, then the size of s + t is lower-bounded by |s| + |t| - 1, unless this quantity is greater than p.

Linearly ordered cancellative semigroups

theorem Finset.card_add_card_sub_nonneg_card_add {α : Type u_1} [LinearOrder α] [AddSemigroup α] [IsCancelAdd α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] {s : Finset α} {t : Finset α} (hs : s.Nonempty) (ht : t.Nonempty) : s.card + t.card - 1 ≤ (s + t).card

The Cauchy-Davenport theorem for linearly ordered additive cancellative semigroups. The size of s + t is lower-bounded by |s| + |t| - 1.

theorem Finset.card_add_card_sub_one_le_card_mul {α : Type u_1} [LinearOrder α] [Semigroup α] [IsCancelMul α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] {s : Finset α} {t : Finset α} (hs : s.Nonempty) (ht : t.Nonempty) : s.card + t.card - 1 ≤ (s * t).card

The Cauchy-Davenport Theorem for linearly ordered cancellative semigroups. The size of s * t is lower-bounded by |s| + |t| - 1.