kakeya_finite

The finite field Kakeya conjecture asserts that any Kakeya set in `𝔽_qⁿ` has size at least `c_n · qⁿ` for some constant `c_n` depending only on `n`. This was first proved by Dvir [Dv08]. The best known bound to date, due to Bukh and Chao [BuCh21], establishes that any Kakeya set in `𝔽_qⁿ` has size at least `qⁿ / (2 - 1/q)^(n - 1)`. [Dv08] Dvir, Z., _On the size of Kakeya sets in finite fields_. Journal of the American Mathematical Society 22 (2009), no. 4, 1093–1097. [BuCh21] Bukh, B. and Chao, T.-W., _Sharp density bounds on the finite field Kakeya problem_. Discrete Analysis 26 (2021), 9 pp.

theorem kakeya_finite {F : Type*} [Field F] [Fintype F] {n : ℕ}
    (K : Finset (Fin n → F)) (hK : IsKakeyaFinite K) :
    card F ^ n / (2 - 1 / card F : ℚ) ^ (n - 1) ≤ K.card

Recent Submissions

No submissions yet. Be the first to attempt this problem.