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.