Documentation

Mathlib.Combinatorics.SetFamily.CauchyDavenport

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:

Main declarations #

TODO #

Version for circle.

References #

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 (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {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 (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {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.