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.

theorem Finset.ruzsa_covering_mul {G : Type u_1} [Group G] {K : ℝ} [DecidableEq G] {A B : Finset G} (hB : B.Nonempty) (hK : ↑(A * B).card ≤ K * ↑B.card) : ∃ F ⊆ A, ↑F.card ≤ K ∧ A ⊆ F * (B / B)

Ruzsa's covering lemma.

theorem Finset.ruzsa_covering_add {G : Type u_1} [AddGroup G] {K : ℝ} [DecidableEq G] {A B : Finset G} (hB : B.Nonempty) (hK : ↑(A + B).card ≤ K * ↑B.card) : ∃ F ⊆ A, ↑F.card ≤ K ∧ A ⊆ F + (B - B)

Ruzsa's covering lemma

@[deprecated]

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) : ∃ F ⊆ A, ↑F.card ≤ K ∧ A ⊆ F * (B / B)

Alias of Finset.ruzsa_covering_mul.

---

Ruzsa's covering lemma.

@[deprecated]

theorem Finset.exists_subset_add_sub {G : Type u_1} [AddGroup G] {K : ℝ} [DecidableEq G] {A B : Finset G} (hB : B.Nonempty) (hK : ↑(A + B).card ≤ K * ↑B.card) : ∃ F ⊆ A, ↑F.card ≤ K ∧ A ⊆ F + (B - B)

theorem Set.ruzsa_covering_mul {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)) : ∃ F ⊆ A, ↑(Nat.card ↑F) ≤ K ∧ A ⊆ F * (B / B) ∧ F.Finite

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

theorem Set.ruzsa_covering_add {G : Type u_1} [AddGroup G] {K : ℝ} {A B : Set G} (hA : A.Finite) (hB : B.Finite) (hB₀ : B.Nonempty) (hK : ↑(Nat.card ↑(A + B)) ≤ K * ↑(Nat.card ↑B)) : ∃ F ⊆ A, ↑(Nat.card ↑F) ≤ K ∧ A ⊆ F + (B - B) ∧ F.Finite

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

@[deprecated]

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)) : ∃ F ⊆ A, ↑(Nat.card ↑F) ≤ K ∧ A ⊆ F * (B / B) ∧ F.Finite

Alias of Set.ruzsa_covering_mul.

---

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

@[deprecated]

theorem Set.exists_subset_add_sub {G : Type u_1} [AddGroup G] {K : ℝ} {A B : Set G} (hA : A.Finite) (hB : B.Finite) (hB₀ : B.Nonempty) (hK : ↑(Nat.card ↑(A + B)) ≤ K * ↑(Nat.card ↑B)) : ∃ F ⊆ A, ↑(Nat.card ↑F) ≤ K ∧ A ⊆ F + (B - B) ∧ F.Finite