Ruzsa's covering lemma #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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_mul_div {α : Type u_1} [decidable_eq α] [comm_group α] (s : finset α) {t : finset α} (ht : t.nonempty) :

∃ (u : finset α), u.card * t.card ≤ (s * t).card ∧ s ⊆ u * t / t

Ruzsa's covering lemma.

source

theorem finset.exists_subset_add_sub {α : Type u_1} [decidable_eq α] [add_comm_group α] (s : finset α) {t : finset α} (ht : t.nonempty) :

∃ (u : finset α), u.card * t.card ≤ (s + t).card ∧ s ⊆ u + t - t

Ruzsa's covering lemma