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.

source

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

source

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.