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 : t.Nonempty) : ∃ (u : Finset α), u.card * t.card ≤ (s + t).card ∧ s ⊆ u + t - t

Ruzsa's covering lemma

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

Ruzsa's covering lemma.

theorem Set.exists_subset_add_sub {α : Type u_1} [AddCommGroup α] {s : Set α} {t : Set α} (hs : Set.Finite s) (ht' : Set.Finite t) (ht : Set.Nonempty t) : ∃ (u : Set α), Nat.card ↑u * Nat.card ↑t ≤ Nat.card ↑(s + t) ∧ s ⊆ u + t - t ∧ Set.Finite u

Ruzsa's covering lemma. Version for sets. For finsets, see Finset.exists_subset_add_sub.

theorem Set.exists_subset_mul_div {α : Type u_1} [CommGroup α] {s : Set α} {t : Set α} (hs : Set.Finite s) (ht' : Set.Finite t) (ht : Set.Nonempty t) : ∃ (u : Set α), Nat.card ↑u * Nat.card ↑t ≤ Nat.card ↑(s * t) ∧ s ⊆ u * t / t ∧ Set.Finite u

Ruzsa's covering lemma for sets. See also Finset.exists_subset_mul_div.