Ruzsa's covering lemma #
This file proves the Ruzsa covering lemma. This says that, for A, B finsets, we can cover A
with at most #(A + B) / #B copies of B - B.
@[deprecated Finset.ruzsa_covering_mul (since := "2024-11-26")]
theorem
Finset.exists_subset_mul_div
{G : Type u_1}
[Group G]
{K : ℝ}
[DecidableEq G]
{A B : Finset G}
(hB : B.Nonempty)
(hK : ↑(A * B).card ≤ K * ↑B.card)
:
Alias of Finset.ruzsa_covering_mul.
Ruzsa's covering lemma.
@[deprecated Set.ruzsa_covering_mul (since := "2024-11-26")]
theorem
Set.exists_subset_mul_div
{G : Type u_1}
[Group G]
{K : ℝ}
{A B : Set G}
(hA : A.Finite)
(hB : B.Finite)
(hB₀ : B.Nonempty)
(hK : ↑(Nat.card ↑(A * B)) ≤ K * ↑(Nat.card ↑B))
:
Alias of Set.ruzsa_covering_mul.
Ruzsa's covering lemma for sets. See also Finset.ruzsa_covering_mul.
@[deprecated Set.ruzsa_covering_add (since := "2024-11-26")]