Fraser: Fourier decay for finite-field Kakeya sets is q^{-1} and sharp
fraser_kakeya_fourier_decay
Submitter: Kim Morrison.
Notes: For every d ≥ 2, every finite-field Kakeya set K ⊆ F_q^d (a subset containing a line in every direction) supports a probability measure μ whose finite-field Fourier transform `μ̂(ξ) = ∑_x χ(-ξ·x) μ(x)` satisfies `‖μ̂(ξ)‖ ≤ q^{-1}` at every nonzero frequency, and this exponent is sharp in every dimension: for every κ ∈ (0, 1) some threshold Q makes the bound `κ · q^{-1}` saturated by every probability measure on a suitable Kakeya set, for every finite field of cardinality ≥ Q. Headline Theorem 2.4 of Fraser, *Fourier analytic properties of Kakeya sets in finite fields*, arXiv:2505.09464.
Source: 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.
Informal solution: For the upper bound, Fraser builds μ as an incidence-weighted measure: choose one affine line through each direction (a `(d, 1)`-set realising the Kakeya property), and weight the resulting union by the appropriate normalised line-counting measure. Expanding `μ̂(ξ)` and applying orthogonality of additive characters along each line — `∑_{a ∈ F_q} χ(a · ⟨ξ, x⟩) = 0` whenever `⟨ξ, x⟩ ≠ 0` — collapses the sum at every nonzero frequency to the residual contribution from directions parallel to `ξ`, yielding the `q^{-1}` bound. For sharpness, Fraser starts with a small planar Kakeya set `K₀ ⊆ F_q²` (an O(q²)-size configuration with the Kakeya property), lifts it to `K = K₀ ⊕ F_q^{d−2} ⊆ F_q^d`, and projects an arbitrary probability measure on `K` down to `F_q²`. A support-size Plancherel argument on the projected measure produces a nonzero frequency at which the Fourier coefficient is at least `(1 − o(1)) · q^{-1}`. Mathlib has `AddChar`, the primitive-character lift `AddChar.FiniteField.primitiveChar_to_Complex`, finite vector-space arithmetic via `Fin d → F`, and `Fintype.card` / finite-sum integration over a finite type, but no finite-field Kakeya theorem, no Salem-set API, no Plancherel for finite abelian groups in the form Fraser uses, and no formalisation of arXiv:2505.09464.
theorem declaration uses `sorry`fraser_kakeya_fourier_decay_and_sharp {d : ℕ} (_hd : 2 ≤ d) {K : Set (LeanEval.Combinatorics.FraserKakeyaProblem.Space F d)} (_hK : LeanEval.Combinatorics.FraserKakeyaProblem.IsKakeya K)
(χ : AddChar F ℂ) (_hχ : χ ≠ 1) :
(∃ μ : LeanEval.Combinatorics.FraserKakeyaProblem.Space F d → ℝ, LeanEval.Combinatorics.FraserKakeyaProblem.IsProbabilityMeasureOn K μ ∧
∀ ξ : LeanEval.Combinatorics.FraserKakeyaProblem.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 (LeanEval.Combinatorics.FraserKakeyaProblem.Space F' d), LeanEval.Combinatorics.FraserKakeyaProblem.IsKakeya K' ∧
∀ μ : LeanEval.Combinatorics.FraserKakeyaProblem.Space F' d → ℝ, LeanEval.Combinatorics.FraserKakeyaProblem.IsProbabilityMeasureOn K' μ →
∃ ξ : LeanEval.Combinatorics.FraserKakeyaProblem.Space F' d, ξ ≠ 0 ∧
κ * (Fintype.card F' : ℝ)⁻¹ ≤
‖fourier (AddChar.FiniteField.primitiveChar_to_Complex F') μ ξ‖) := F:Type u_1inst✝²:Field Finst✝¹:Fintype Finst✝:DecidableEq Fd:ℕ_hd:2 ≤ dK:Set (Space F d)_hK:IsKakeya Kχ:AddChar F ℂ_hχ:χ ≠ 1⊢ (∃ μ,
IsProbabilityMeasureOn K μ ∧
∀ (ξ : Space F d), ξ ≠ 0 → ‖LeanEval.Combinatorics.FraserKakeyaProblem.fourier χ μ ξ‖ ≤ (↑(Fintype.card F))⁻¹) ∧
∀ (κ : ℝ),
0 < κ →
κ < 1 →
∃ Q,
∀ (F' : Type u_2) [inst : Field F'] [inst_1 : Fintype F'] [DecidableEq F'],
Q ≤ Fintype.card F' →
∃ K',
IsKakeya K' ∧
∀ (μ : Space F' d → ℝ),
IsProbabilityMeasureOn K' μ →
∃ ξ,
ξ ≠ 0 ∧
κ * (↑(Fintype.card F'))⁻¹ ≤
‖LeanEval.Combinatorics.FraserKakeyaProblem.fourier
(AddChar.FiniteField.primitiveChar_to_Complex F') μ ξ‖
All goals completed! 🐙Solved by
• @GanjinZero with Seed Prover (ByteDance) on Jun 2, 2026
• @mayorov-m-a with Aleph Prover(logicalintelligence.com) on Jun 3, 2026
• @LorenzoLuccioli with Aristotle (Harmonic) on Jun 3, 2026