Kakeya problem

Reference: Wikipedia

def Kakeya.IsKakeya {n : ℕ} (S : Set (EuclideanSpace ℝ (Fin n))) : Prop

A set S in ℝⁿ is called a Kakeya set if it contains a unit line segment in every direction. For simplicity, we omit the compactness assumption here. For a discussion on the equivalence of definitions with and without compactness, see this paper.

Equations

• Kakeya.IsKakeya S = ∀ (v : EuclideanSpace ℝ (Fin n)), ‖v‖ = 1 → ∃ (a : EuclideanSpace ℝ (Fin n)), affineSegment ℝ a (a + v) ⊆ S

theorem Kakeya.isKakeya_closedBall (n : ℕ) : IsKakeya (Metric.closedBall 0 1)

A trivial example: the closed ball of radius 1 in ℝⁿ is a Kakeya set.

def Kakeya.KakeyaSetConjectureDim (n : ℕ) : Prop

The Kakeya set conjecture in dimension n: the statement that every Kakeya set in ℝⁿ has Hausdorff dimension n.

Equations

• Kakeya.KakeyaSetConjectureDim n = ∀ (S : Set (EuclideanSpace ℝ (Fin n))), Kakeya.IsKakeya S → dimH S = ↑n

theorem Kakeya.kakeya_set_conjecture (n : ℕ) (hn : n > 0) : KakeyaSetConjectureDim n

theorem Kakeya.kakeya_2d : KakeyaSetConjectureDim 2

The two-dimensional case, proved by Davies [Da71].

[Da71] Davies, R. O., Some remarks on the Kakeya problem. Math. Proc. Cambridge Philos. Soc. 69 (1971), no. 3, 417–421.

theorem Kakeya.kakeya_3d : KakeyaSetConjectureDim 3

The three-dimensional case, proved by Wang, Zahl [WaZa25].

[WaZa25] Wang, H. and Zahl, J., Volume estimates for unions of convex sets, and the Kakeya set conjecture in three dimensions. arXiv preprint, arXiv:2502.17655, 2025.

def Kakeya.IsKakeyaFinite {F : Type u_1} [Field F] [Fintype F] {n : ℕ} (S : Finset (Fin n → F)) : Prop

A finite field variant of the Kakeya problem considers subsets of 𝔽_qⁿ that contain a line in every direction.

Equations

• Kakeya.IsKakeyaFinite S = ∀ (v : Fin n → F), v ≠ 0 → ∃ (a : Fin n → F), ∀ (t : F), a + t • v ∈ S

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

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.