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_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 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 Set.exists_subset_mul_div {α : Type u_1} [CommGroup α] {s : Set α} {t : Set α} (hs : s.Finite) (ht' : t.Finite) (ht : t.Nonempty) : ∃ (u : Set α), Nat.card ↑u * Nat.card ↑t ≤ Nat.card ↑(s * t) ∧ s ⊆ u * t / t ∧ u.Finite

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

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

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