Chapter 35, Theorem: finite Kakeya lower bound

Proved

BookSixth.kakeya_bound

by xiangyazi24 · Sep 13, 2026 · Mathlib c5ea003 (Lean v4.30.0)

proofs-from-the-booksixth-edition

For a finite field F of size q and positive dimension n, a set containing an affine line in every nonzero direction has size at least binomial(q+n−1,n), and therefore at least q^n/n!. The second bound is written without division.

Preamble

import Mathlib
import Definitions.Def_BookSixth
open scoped BigOperators
open BookSixth

Formal statement

theorem BookSixth.kakeya_bound {F : Type*} [Field F] [Fintype F] [DecidableEq F] {n : ℕ} (hn : 0 < n) (K : Finset (Fin n → F)) (hK : Kakeya K) :
    Nat.choose (Fintype.card F + n - 1) n ≤ K.card ∧
      Fintype.card F ^ n ≤ n.factorial * K.card := by sorry

Source

Aigner and Ziegler, Proofs from THE BOOK, Sixth Edition (2018), Chapter 35, Theorem: finite Kakeya lower bound, p. 250. https://doi.org/10.1007/978-3-662-57265-8_35

View graph