Documentation

Mathlib.Combinatorics.Additive.RuzsaCovering

Ruzsa's covering lemma #

This file proves the Ruzsa covering lemma. This says that, for s, t finsets, we can cover s with at most (s + t).card / t.card copies of t - t.

TODO #

Merge this file with other prerequisites to Freiman's theorem once we have them.

theorem Finset.exists_subset_add_sub {α : Type u_1} [DecidableEq α] [AddCommGroup α] (s : Finset α) {t : Finset α} (ht : Finset.Nonempty t) :
u, Finset.card u * Finset.card t Finset.card (s + t) s u + t - t

Ruzsa's covering lemma

theorem Finset.exists_subset_mul_div {α : Type u_1} [DecidableEq α] [CommGroup α] (s : Finset α) {t : Finset α} (ht : Finset.Nonempty t) :
u, Finset.card u * Finset.card t Finset.card (s * t) s u * t / t

Ruzsa's covering lemma.