The Cauchy-Davenport theorem

Derives the Cauchy-Davenport theorem cauchy_davenport on sumsets in ZMod p from the Alon-Nathanson-Ruzsa polynomial method.

theorem sum_fin_two {M : Type u_2} [AddCommMonoid M] (f : Fin 2 → M) : ∑ i : Fin 2, f i = f 0 + f 1

theorem binomial_coeff_ne_zero_mod_p {p : ℕ} [Fact (Nat.Prime p)] (n k : ℕ) (hp : Nat.Prime p) (h_k : k ≤ n) (h_n : n < p) : ↑(n.choose k) ≠ 0

def sumset {α : Type u_2} [Add α] [DecidableEq α] (A B : Finset α) : Finset α

The sumset A + B = { a + b | a ∈ A, b ∈ B } as a Finset.

Equations

• sumset A B = Finset.image (fun (x : α × α) => x.1 + x.2) (A ×ˢ B)

theorem cauchy_davenport_small_sum {p : ℕ} [Fact (Nat.Prime p)] (A B S : Finset (ZMod p)) (hp : Nat.Prime p) (hA : A.Nonempty) (hB : B.Nonempty) (h_sum : A.card + B.card ≤ p + 1) (hS : S = sumset A B) : S.card ≥ A.card + B.card - 1

theorem cauchy_davenport {p : ℕ} [Fact (Nat.Prime p)] (A B S : Finset (ZMod p)) (hp : Nat.Prime p) (hA : A.Nonempty) (hB : B.Nonempty) (hS : S = sumset A B) : min p (A.card + B.card - 1) ≤ S.card