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

• cauchy_davenport_minOrder_mul: A generalisation of the Cauchy-Davenport theorem to arbitrary groups.
• cauchy_davenport_of_isTorsionFree: The Cauchy-Davenport theorem in torsion-free groups.
• ZMod.cauchy_davenport: The Cauchy-Davenport theorem for ZMod p.
• cauchy_davenport_mul_of_linearOrder_isCancelMul: 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 cauchy_davenport_minOrder_mul {α : Type u_2} [Group α] [DecidableEq α] {s 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 cauchy_davenport_minOrder_add {α : Type u_2} [AddGroup α] [DecidableEq α] {s 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 cauchy_davenport_of_isMulTorsionFree {G : Type u_1} [DecidableEq G] [Group G] [IsMulTorsionFree G] {s t : Finset G} (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 cauchy_davenport_of_isAddTorsionFree {G : Type u_1} [DecidableEq G] [AddGroup G] [IsAddTorsionFree G] {s t : Finset G} (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.

@[deprecated cauchy_davenport_of_isMulTorsionFree (since := "2025-04-23")]

theorem cauchy_davenport_mul_of_isTorsionFree {G : Type u_1} [DecidableEq G] [Group G] [IsMulTorsionFree G] {s t : Finset G} (hs : s.Nonempty) (ht : t.Nonempty) : s.card + t.card - 1 ≤ (s * t).card

Alias of cauchy_davenport_of_isMulTorsionFree.

---

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

@[deprecated cauchy_davenport_of_isMulTorsionFree (since := "2025-04-23")]

theorem cauchy_davenport_add_of_isTorsionFree {G : Type u_1} [DecidableEq G] [AddGroup G] [IsAddTorsionFree G] {s t : Finset G} (hs : s.Nonempty) (ht : t.Nonempty) : s.card + t.card - 1 ≤ (s + t).card

$$ℤ/nℤ$$

theorem ZMod.cauchy_davenport {p : ℕ} (hp : Nat.Prime p) {s 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 cauchy_davenport_mul_of_linearOrder_isCancelMul {α : Type u_2} [LinearOrder α] [Mul α] [IsCancelMul α] [MulLeftMono α] [MulRightMono α] {s 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.

theorem cauchy_davenport_add_of_linearOrder_isCancelAdd {α : Type u_2} [LinearOrder α] [Add α] [IsCancelAdd α] [AddLeftMono α] [AddRightMono α] {s 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.