Kakeya sets

TheoremBesicovitch's Kakeya set of measure zero#✓fully proved

There is a compact set \(K \subseteq \mathbb{R}^2\) of Lebesgue measure zero that contains a unit segment in every direction: \(K\) is measurable, and for every unit vector \(v \in \mathbb{R}^2\) there is a point \(a \in \mathbb{R}^2\) with \(a + t v \in K\) for all \(t \in [0, 1]\).

The proof here follows T. W. Körner, "Besicovitch via Baire", Studia Math. 158 (2003): a Baire-category argument in the Hausdorff metric space of compact sets, not a Perron-tree construction.

public theorem besicovitch_kakeya_compact_measure_zero
    [MeasurableSpace (EuclideanSpace ℝ (Fin 2))]
    [BorelSpace (EuclideanSpace ℝ (Fin 2))] :
    ∃ (K : Set (EuclideanSpace ℝ (Fin 2))),
      MeasurableSet K ∧ IsCompact K ∧
        ((volume : Measure (EuclideanSpace ℝ (Fin 2))) K = 0) ∧
        ∀ (v : EuclideanSpace ℝ (Fin 2)), ‖v‖ = 1 →
          ∃ (a : EuclideanSpace ℝ (Fin 2)), ∀ t ∈ Set.Icc (0 : ℝ) 1, a + t • v ∈ K

Sources

• A. S. Besicovitch, Math. Z. 27 (1928) 312–320 and S. Kakeya, Tohoku Rep. 6 (1917); Perron-tree gives compact measure-zero Kakeya set; Lean states compact Lebesgue-null oriented version in ℝ² with segments a+t•v, t∈[0, 1].

AbbreviationThree-dimensional Euclidean space#✓fully proved

The space \(\mathbb{R}^3\) with the Euclidean inner product.

abbrev Space := EuclideanSpace ℝ (Fin 3)

Used by 2

Used byKakeya set · Wang–Zahl theorem: the Kakeya conjecture in three dimensions

DefinitionKakeya set#✓fully proved

A Kakeya set is a compact subset \(K\) of three-dimensional Euclidean space that contains a unit line segment in every direction: for every unit vector \(v\) there is a point \(x\) with \(x + t v \in K\) for all \(t \in [0, 1]\).

def IsKakeya (K : Set Space) : Prop :=
  IsCompact K ∧
    ∀ v : Space, ‖v‖ = 1 →
      ∃ x : Space, ∀ t : ℝ, t ∈ Set.Icc 0 1 → x + t • v ∈ K

Uses 1 · Used by 1

Statement usesThree-dimensional Euclidean space

Used byWang–Zahl theorem: the Kakeya conjecture in three dimensions

TheoremWang–Zahl theorem: the Kakeya conjecture in three dimensions#●ready to prove

Every Kakeya set in three-dimensional Euclidean space has Hausdorff dimension \(3\).

public theorem_wanted wang_zahl_kakeya_dimH {K : Set Space} (hK : IsKakeya K) :
    dimH K = 3

Sources

• H. Wang and J. Zahl, 'Volume estimates for unions of convex sets, and the Kakeya set conjecture in three dimensions', Theorem 1.1, arXiv:2502.17655 (2025), https://arxiv.org/abs/2502.17655. The proof builds on their 'Sticky Kakeya sets and the sticky Kakeya conjecture', arXiv:2210.09581, and 'The Assouad dimension of Kakeya sets in R^3', arXiv:2401.12337. Problem wang_zahl_kakeya_dimH of the lean-eval benchmark.

Uses 2

Statement usesKakeya set · Three-dimensional Euclidean space

3 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.