Green's Open Problem 39

References:

• [Gr24] Green, Ben. "100 open problems." (2024).
• [BJR11] Bollobás, Béla, Svante Janson, and Oliver Riordan. "On covering by translates of a set." Random Structures & Algorithms 38.1‐2 (2011): 33-67.

def Green39.proportionCoverable (p k c : ℕ) : ℚ

The proportion of subsets of $\mathbb{Z}/p\mathbb{Z}$ of size $k$ that can cover $\mathbb{Z}/p\mathbb{Z}$ using at most $c$ translates.

If p = 0 or k > p, return 0 by convention.

Equations

• One or more equations did not get rendered due to their size.

theorem Green39.proportionCoverable_p_p_1 : proportionCoverable 3 3 1 = 1

theorem Green39.proportionCoverable_t_0 : proportionCoverable 5 2 0 = 0

theorem Green39.proportionCoverable_2_1_2 : proportionCoverable 2 1 2 = 1

theorem Green39.proportionCoverable_3_1_2 : proportionCoverable 3 1 2 = 0

theorem Green39.proportionCoverable_a_gt_p : proportionCoverable 3 4 2 = 0

theorem Green39.proportionCoverable_7_4_2 : proportionCoverable 7 4 2 = 3 / 5

theorem Green39.proportionCoverable_11_3_4 : proportionCoverable 11 3 4 = 1 / 3

theorem Green39.proportionCoverable_11_4_3 : proportionCoverable 11 4 3 = 1 / 6

theorem Green39.green_39 : True ↔ Filter.Tendsto (fun (p : { q : ℕ // Nat.Prime q }) => have k := (↑p).sqrt; have c := 100 * k; ↑(proportionCoverable (↑p) k c)) Filter.atTop (nhds 1)

If $A \subset \mathbb{Z}/p\mathbb{Z}$ is random, $|A| = \sqrt{p}$, can we almost surely cover $\mathbb{Z}/p\mathbb{Z}$ with $100\sqrt{p}$ translates of $A$? [Gr24]

theorem Green39.green_39.variant_101 : True ↔ Filter.Tendsto (fun (p : { q : ℕ // Nat.Prime q }) => have k := (↑p).sqrt; have c := ⌊1.01 * ↑k⌋₊; ↑(proportionCoverable (↑p) k c)) Filter.atTop (nhds 1)

"I do not know how to answer this even with 100 replaced by 1.01." [Gr24]"

theorem Green39.green_39.variant_theta : True ↔ ∀ (θ : ℝ), 0 < θ → θ ≤ 1 / 2 → ∃ C > 1, Filter.Tendsto (fun (p : { q : ℕ // Nat.Prime q }) => have k := ⌊↑↑p ^ θ⌋₊; have c := ⌊C * ↑↑p ^ θ⌋₊; ↑(proportionCoverable (↑p) k c)) Filter.atTop (nhds 1)

Similar questions are interesting with $\sqrt{p}$ replaced by $p^\theta$ for any $\theta \le 1/2$. [Gr24]