Kakeya sets in finite fields

AbbreviationCoordinate space#✓fully proved

For a type \(F\) and a natural number \(d\), \(F^d\) denotes the set of \(d\)-tuples \((x_1, \dots, x_d)\) of elements of \(F\), that is, functions from a \(d\)-element index set to \(F\).

Here \(F\) is a finite field, so \(F^d\) is the \(d\)-dimensional vector space over \(F\).

abbrev Space (F : Type*) (d : ℕ) := Fin d → F

Used by 6

Used byAffine line · Dot product · Finite-field Fourier transform · Fraser's Fourier decay theorem for finite-field Kakeya sets · Kakeya set · Probability measure supported on a set

DefinitionDot product#✓fully proved

Let \(F\) be a finite field and \(d\) a natural number. For \(x, y \in F^d\), the dot product is \(x \cdot y = \sum_{i} x_i y_i \in F\), the sum running over the \(d\) coordinates.

def dot {d : ℕ} (x y : Space F d) : F :=
  ∑ i, x i * y i

Uses 1 · Used by 1

Statement usesCoordinate space

Used byFinite-field Fourier transform

DefinitionAffine line#✓fully proved

Let \(F\) be a finite field and \(d\) a natural number. For \(y, x \in F^d\), the affine line with base point \(y\) and direction \(x\) is the set \(\{y + a x : a \in F\} \subseteq F^d\). When \(x = 0\) this set is the single point \(\{y\}\).

def affineLine {d : ℕ} (y x : Space F d) : Set (Space F d) :=
  {z | ∃ a : F, z = y + a • x}

Uses 1 · Used by 1

Statement usesCoordinate space

Used byKakeya set

DefinitionKakeya set#✓fully proved

Let \(F\) be a finite field and \(d\) a natural number. A set \(K \subseteq F^d\) is a Kakeya set if for every \(x \in F^d\) there is \(y \in F^d\) such that the affine line \(\{y + a x : a \in F\}\) is contained in \(K\); that is, \(K\) contains a line in every direction.

def IsKakeya {d : ℕ} (K : Set (Space F d)) : Prop :=
  ∀ x : Space F d, ∃ y : Space F d, affineLine y x ⊆ K

Uses 2 · Used by 2

Statement usesCoordinate space · Affine line

Used byStatement of the finite field Kakeya bound in dimension three · Fraser's Fourier decay theorem for finite-field Kakeya sets

DefinitionProbability measure supported on a set#✓fully proved

Let \(F\) be a finite field, \(d\) a natural number and \(K \subseteq F^d\). A function \(\mu : F^d \to \mathbb{R}\) is a probability measure on \(K\) if \(\mu(x) \ge 0\) for every \(x \in F^d\), \(\sum_{x \in F^d} \mu(x) = 1\), and \(\mu(x) \ne 0\) implies \(x \in K\).

def IsProbabilityMeasureOn {d : ℕ} (K : Set (Space F d))
    (μ : Space F d → ℝ) : Prop :=
  (∀ x, 0 ≤ μ x) ∧ (∑ x, μ x = 1) ∧ ∀ x, μ x ≠ 0 → x ∈ K

Uses 1 · Used by 1

Statement usesCoordinate space

Used byFraser's Fourier decay theorem for finite-field Kakeya sets

DefinitionFinite-field Fourier transform#✓fully proved

Let \(F\) be a finite field, \(d\) a natural number and \(\chi\) an additive character of \(F\) with values in \(\mathbb{C}\). For \(\mu : F^d \to \mathbb{R}\) and \(\xi \in F^d\), the Fourier transform of \(\mu\) at \(\xi\) is \(\hat{\mu}(\xi) = \sum_{x \in F^d} \chi(-\xi \cdot x)\, \mu(x) \in \mathbb{C}\), where \(\xi \cdot x\) is the dot product.

The definition allows any character; it is used with a nontrivial one.

noncomputable def fourier {d : ℕ} (χ : AddChar F ℂ) (μ : Space F d → ℝ)
    (ξ : Space F d) : ℂ :=
  ∑ x, χ (-(dot ξ x)) * (μ x : ℂ)

Uses 2 · Used by 1

Statement usesCoordinate space · Dot product

Used byFraser's Fourier decay theorem for finite-field Kakeya sets

TheoremFraser's Fourier decay theorem for finite-field Kakeya sets#●ready to prove

Let \(F\) be a finite field with \(q\) elements, let \(d \ge 2\) be a natural number, let \(K \subseteq F^d\) be a Kakeya set and let \(\chi\) be a nontrivial additive character of \(F\) with values in \(\mathbb{C}\). Then, first, there is a probability measure \(\mu\) on \(K\) whose Fourier transform \(\hat{\mu}\) with respect to \(\chi\) satisfies \(|\hat{\mu}(\xi)| \le q^{-1}\) for every nonzero \(\xi \in F^d\). Second, this bound is sharp: for every real \(\kappa\) with \(0 < \kappa < 1\) there is a natural number \(Q\) such that for every finite field \(F'\) with \(q' \ge Q\) elements there is a Kakeya set \(K' \subseteq (F')^d\) such that every probability measure \(\mu\) on \(K'\) has a nonzero \(\xi \in (F')^d\) at which its Fourier transform \(\hat{\mu}\) with respect to a fixed primitive additive character of \(F'\) satisfies \(|\hat{\mu}(\xi)| \ge \kappa \, q'^{-1}\).

public theorem_wanted fraser_kakeya_fourier_decay_and_sharp
    {d : ℕ} (_hd : 2 ≤ d) {K : Set (Space F d)} (_hK : IsKakeya K)
    (χ : AddChar F ℂ) (_hχ : χ ≠ 1) :
    (∃ μ : Space F d → ℝ, IsProbabilityMeasureOn K μ ∧
      ∀ ξ : Space F d, ξ ≠ 0 →
        ‖fourier χ μ ξ‖ ≤ (Fintype.card F : ℝ)⁻¹) ∧
    (∀ κ : ℝ, 0 < κ → κ < 1 →
      ∃ Q : ℕ, ∀ (F' : Type*) [Field F'] [Fintype F'] [DecidableEq F'],
        Q ≤ Fintype.card F' →
          ∃ K' : Set (Space F' d), IsKakeya K' ∧
            ∀ μ : Space F' d → ℝ, IsProbabilityMeasureOn K' μ →
              ∃ ξ : Space F' d, ξ ≠ 0 ∧
                κ * (Fintype.card F' : ℝ)⁻¹ ≤
                  ‖fourier (AddChar.FiniteField.primitiveChar_to_Complex F') μ ξ‖)

Sources

• J.M. Fraser, 'Fourier analytic properties of Kakeya sets in finite fields', Bull. London Math. Soc. 58(5) (2026); DOI 10.1112/blms.70367; arXiv:2505.09464. Problem fraser_kakeya_fourier_decay of the lean-eval benchmark.

Uses 4

Statement usesKakeya set · Probability measure supported on a set · Coordinate space · Finite-field Fourier transform

DefinitionStatement of the finite field Kakeya bound in dimension three#✓fully proved

This is the statement that there is a real number \(c > 0\) such that for every finite field \(F\) and every Kakeya set \(E \subseteq F^3\), that is, a set such that for every \(x \in F^3\) there is \(y \in F^3\) with \(\{y + a x : a \in F\} \subseteq E\), we have \(|E| \ge c\,|F|^3\).

This is Dvir's form of Tao's question (AIM, Recent trends in additive combinatorics, Problem 3.8), which asks for \(|E| \gtrsim |F|^{5/2 + \varepsilon}\) for some \(\varepsilon > 0\); the exponent \(3\) gives \(\varepsilon = 1/2\).

def finiteFieldKakeyaCubeLowerBound : Prop :=
  ∃ c : ℝ, 0 < c ∧ ∀ (F : Type) [Field F] [Fintype F] [DecidableEq F] (E : Finset (Fin 3 → F)),
    IsKakeya (F := F) (d := 3) (E : Set (Fin 3 → F)) → c * (Fintype.card F : ℝ) ^ 3 ≤ E.card

Uses 1 · Used by 1

Statement usesKakeya set

Used byFinite field Kakeya sets in dimension three have cubic size

TheoremFinite field Kakeya sets in dimension three have cubic size#●ready to prove

There is a real number \(c > 0\) such that for every finite field \(F\) and every Kakeya set \(E \subseteq F^3\), that is, a set such that for every \(x \in F^3\) there is \(y \in F^3\) with \(\{y + a x : a \in F\} \subseteq E\), we have \(|E| \ge c\,|F|^3\).

Dvir proved by the polynomial method that every Kakeya set \(K \subseteq F^n\) over a finite field \(F\) with \(q\) elements has \(|K| \ge C_n q^n\), with \(C_n\) depending only on \(n\) (Theorem 3, the Alon–Tao form of his Theorem 1). For \(n = 3\) this answers Tao's question, which asks for \(|E| \gtrsim |F|^{5/2 + \varepsilon}\) for some \(\varepsilon > 0\), beyond Wolff's bound \(|F|^{5/2}\), with \(\varepsilon = 1/2\).

public theorem_wanted finiteFieldKakeyaCubeLowerBound_holds : finiteFieldKakeyaCubeLowerBound

Sources

• AIM workshop Recent trends in additive combinatorics (2004), problem list collected by E. Croot and V. F. Lev, https://aimath.org/WWN/additivecomb/additivecomb.pdf, Problem 3.8 (T. Tao); resolution: Z. Dvir, On the size of Kakeya sets in finite fields, J. Amer. Math. Soc. 22 (2009), 1093-1097, arXiv:0803.2336, Theorem 3 (Section 1.1, the Alon-Tao improvement of Theorem 1): every Kakeya set K ⊂ Fⁿ satisfies |K| ≥ C_n qⁿ with C_n depending only on n; for n = 3 this is |K| ≫ q³, https://doi.org/10.1090/S0894-0347-08-00607-3.

Uses 1

Statement usesStatement of the finite field Kakeya bound in dimension three

7 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.